I think this is something Gauss could have proved, and the point is to come up with his sort of proof. I'm not seeing that as too hard. To show a polynomial of degree at least 1 is transcendental over K is easy. The harder step is to do that for rational functions P/Q, where the degree should be defined as the maximum of degree P and degree Q. So by rationalising we need to look at F(P, Q) where F is a general binary form (well, you should start with a monic polynomial to get to F, is what I mean). In the case of unequal degrees there is an easy reason why this can't be zero, looking at the top power of t. So we should assume equal degrees. But then P/Q can be written as a constant plus a term with unequal degrees, by long division of polynomials. That looks like the inductive step in a proof, by induction on the degree.

Presumably you would want to express the idea that K(P/Q) and K(t) are then isomorphic in some other fashion, but I don't know quite what you have in mind.

**Edit:** In reply to the comment: we want to prove unirational implies rational for curves C, as geometers would put it. So far we have enough to prove C has a non-constant rational map to the projective line L. This clearly isn't enough yet, but the work involved can be reduced to some finiteness statement. It would be enough to show that there are only finitely many intermediate fields, i.e. "curves" C, for a given rational map L -> L. That statement is known to imply the primitive element theorem over infinite fields, by a box principle argument. Abstract field theory takes us to Steinitz, away from Gauss indeed (and Luroth, really). Without at least the ACC for subfields in this case, how are we going to prove that a general subfield is finitely generated? I ask because we don't really have a clear statement from the OP about how many limbs we have to tie behind our backs here.

purely transcendentalextension (necessarily simple, by comparison of transcendence degrees). This requires some discussion of fields including the distinction between algebraic and transcendental extensions. – Jim Humphreys Jun 6 '11 at 17:38