let f be Field-yielding ascending sequence ; :: thesis: for i, j being Element of NAT st i <= j holds
f . j is FieldExtension of f . i
let i, j be Element of NAT ; :: thesis: ( i <= j implies f . j is FieldExtension of f . i )
assume AS: i <= j ; :: thesis: f . j is FieldExtension of f . i
defpred S₁[ Nat] means ex k being Element of NAT st
( k = i + $1 & f . k is FieldExtension of f . i );
IA: S₁[ 0 ]

proof

take k = i; :: thesis: ( k = i + 0 & f . k is FieldExtension of f . i )
thus ( k = i + 0 & f . k is FieldExtension of f . i ) by FIELD_4:6; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider n being Element of NAT such that
IV: ( n = i + k & f . n is FieldExtension of f . i ) ;
f . (n + 1) is FieldExtension of f . n by defasc;
hence S₁[k + 1] by IV; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H: i + n = j by AS, NAT_1:10;
S₁[n] by I;
hence f . j is FieldExtension of f . i by H; :: thesis: verum