let f be Field-yielding ascending sequence ; :: thesis: for X being finite Subset of (SeqField f) ex i being Element of NAT st X c= the carrier of (f . i)
let X be finite Subset of (SeqField f); :: thesis: ex i being Element of NAT st X c= the carrier of (f . i)
defpred S₁[ Nat] means for X being finite Subset of (SeqField f) st card X = $1 holds
ex i being Element of NAT st X c= the carrier of (f . i);
set F = SeqField f;
H: the carrier of (SeqField f) = Carrier f by dsf
.= union { the carrier of (f . i) where i is Element of NAT : verum } ;
IA: S₁[ 0 ]

proof

now :: thesis: for X being finite Subset of (SeqField f) st card X = 0 holds
ex i being Element of NAT st X c= the carrier of (f . i)

let X be finite Subset of (SeqField f); :: thesis: ( card X = 0 implies ex i being Element of NAT st X c= the carrier of (f . i) )
assume card X = 0 ; :: thesis: ex i being Element of NAT st X c= the carrier of (f . i)
then X c= the carrier of (f . 0) ;
hence ex i being Element of NAT st X c= the carrier of (f . i) ; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

I1: S₁[1]

proof

now :: thesis: for X being finite Subset of (SeqField f) st card X = 1 holds
ex i being Element of NAT st X c= the carrier of (f . i)

let X be finite Subset of (SeqField f); :: thesis: ( card X = 1 implies ex i being Element of NAT st X c= the carrier of (f . i) )
assume card X = 1 ; :: thesis: ex i being Element of NAT st X c= the carrier of (f . i)
then consider a being object such that
A: X = {a} by CARD_2:42;
a in X by A, TARSKI:def 1;
then reconsider a = a as Element of (SeqField f) ;
consider Y being set such that
B: ( a in Y & Y in { the carrier of (f . i) where i is Element of NAT : verum } ) by H, TARSKI:def 4;
consider i being Element of NAT such that
C: Y = the carrier of (f . i) by B;
X c= the carrier of (f . i) by A, B, C, TARSKI:def 1;
hence ex i being Element of NAT st X c= the carrier of (f . i) ; :: thesis: verum

end;

hence S₁[1] ; :: 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 IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for X being finite Subset of (SeqField f) st card X = k + 1 holds
ex i being Element of NAT st X c= the carrier of (f . i)

let X be finite Subset of (SeqField f); :: thesis: ( card X = k + 1 implies ex i being Element of NAT st i c= the carrier of (f . b₂) )
assume AS: card X = k + 1 ; :: thesis: ex i being Element of NAT st i c= the carrier of (f . b₂)
then A: X <> {} ;
set a = the Element of X;
A1: the Element of X in X by A;
then reconsider a = the Element of X as Element of (SeqField f) ;
set X1 = X \ {a};
a in {a} by TARSKI:def 1;
then not a in X \ {a} by XBOOLE_0:def 5;
then B: card ((X \ {a}) \/ {a}) = (card (X \ {a})) + 1 by CARD_2:41;
{a} c= X by A1, TARSKI:def 1;
then C: (X \ {a}) \/ {a} = X by FIELD_5:1;
then consider i1 being Element of NAT such that
D: X \ {a} c= the carrier of (f . i1) by AS, B, IV;
card {a} = 1 by CARD_2:42;
then consider i2 being Element of NAT such that
E: {a} c= the carrier of (f . i2) by I1;
a in {a} by TARSKI:def 1;
then reconsider a = a as Element of (f . i2) by E;

per cases ( i1 <= i2 or i2 <= i1 ) ;

suppose i1 <= i2 ; :: thesis: ex i being Element of NAT st i c= the carrier of (f . b₂)

then f . i2 is FieldExtension of f . i1 by lem3;
then f . i1 is Subfield of f . i2 by FIELD_4:7;
then the carrier of (f . i1) c= the carrier of (f . i2) by EC_PF_1:def 1;
then X \ {a} c= the carrier of (f . i2) by D;
then (X \ {a}) \/ {a} c= the carrier of (f . i2) \/ the carrier of (f . i2) by XBOOLE_1:13;
hence ex i being Element of NAT st X c= the carrier of (f . i) by C; :: thesis: verum

end;

suppose i2 <= i1 ; :: thesis: ex i being Element of NAT st i c= the carrier of (f . b₂)

then reconsider a = a as Element of (f . i1) by lem1;
(X \ {a}) \/ {a} c= the carrier of (f . i1) \/ the carrier of (f . i1) by D, XBOOLE_1:13;
hence ex i being Element of NAT st X c= the carrier of (f . i) by C; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
I2: card X = n ;
consider i being Element of NAT such that
H: X c= the carrier of (f . i) by I, I2;
thus ex i being Element of NAT st X c= the carrier of (f . i) by H; :: thesis: verum