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

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 & a in the carrier of (f . n) ) ;
f . (n + 1) is FieldExtension of f . n by defasc;
then f . n is Subring of f . (n + 1) by FIELD_4:def 1;
then the carrier of (f . n) c= the carrier of (f . (n + 1)) by C0SP1:def 3;
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 a in the carrier of (f . j) by H; :: thesis: verum