let K1 be Subfield of F_Rat ; :: thesis: NAT c= the carrier of K1
set C1 = the carrier of K1;
defpred S₁[ Nat] means $1 in the carrier of K1;
0. F_Rat = 0 ;
then 0. K1 = 0 by EC_PF_1:def 1;
then A1: S₁[ 0 ] ;

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
A4: 1. K1 = 1. F_Rat by EC_PF_1:def 1
.= 1 ;
A5: the addF of K1 = the addF of F_Rat || the carrier of K1 by EC_PF_1:def 1;
the addF of K1 . (1,n) = addrat . (1,n) by A3, A4, A5, FUNCT_1:49, ZFMISC_1:87
.= 1 + n by BINOP_2:def 15 ;
hence S₁[n + 1] by A3, A4, BINOP_1:17; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence NAT c= the carrier of K1 ; :: thesis: verum