consider f being Function such that
A4: ( dom f = card F2() & ( for x being object st x in card F2() holds
f . x = F1(x) ) ) from FUNCT_1:sch 3();
 defpred S1[ Nat] means ( $1 < card F2() implies F1($1) in F2() );
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume that
A6: ( n < card F2() implies F1(n) in F2() ) and
A7: n + 1 < card F2() and
A8: not F1((n + 1)) in F2() ; :: thesis: contradiction
consider f being Function such that
A9: ( dom f = n + 1 & ( for x being object st x in n + 1 holds
f . x = F1(x) ) ) from FUNCT_1:sch 3();
 A10: n + 1 = { k where k is Nat : k < n + 1 } by AXIOMS:4;
A11: n <= n + 1 by NAT_1:11;
A12: rng f = F2()
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: F2() c= rng f
let x be object ; :: thesis: ( x in rng f implies x in F2() )
assume x in rng f ; :: thesis: x in F2()
then consider y being object such that
A13: y in n + 1 and
A14: x = f . y by A9, FUNCT_1:def 3;
consider k being Nat such that
A15: y = k and
A16: k < n + 1 by A10, A13;
reconsider k = k as Nat ;
k <= n by A16, NAT_1:13;
then ( k = n or k < n ) by XXREAL_0:1;
then F1(k) in F2() by A2, A6, A7, A11, XXREAL_0:2;
hence x in F2() by A9, A13, A14, A15; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F2() or x in rng f )
assume A17: x in F2() ; :: thesis: x in rng f
then consider k being Nat such that
A18: x = F1(k) by A1;
now :: thesis: not k >= n + 1
assume k >= n + 1 ; :: thesis: contradiction
then ( k = n + 1 or k > n + 1 ) by XXREAL_0:1;
hence contradiction by A2, A8, A17, A18; :: thesis: verum
end;
then A19: k in n + 1 by A10;
then x = f . k by A9, A18;
hence x in rng f by A9, A19, FUNCT_1:def 3; :: thesis: verum
end;
f is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A20: x1 in dom f and
A21: x2 in dom f and
A22: f . x1 = f . x2 ; :: thesis: x1 = x2
( ex k being Nat st
( x1 = k & k < n + 1 ) & ex k being Nat st
( x2 = k & k < n + 1 ) ) by A9, A10, A20, A21;
then A23: ( F1(x1) = F1(x2) implies x1 = x2 ) by A3;
F1(x1) = f . x1 by A9, A20;
hence x1 = x2 by A9, A21, A22, A23; :: thesis: verum
end;
then n + 1,F2() are_equipotent by A9, A12, WELLORD2:def 4;
hence contradiction by A7, CARD_1:def 2; :: thesis: verum
end;
A24: card F2() = { n where n is Nat : n < card F2() } by AXIOMS:4;
f is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A25: x1 in dom f and
A26: x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
( ex k being Nat st
( x1 = k & k < card F2() ) & ex k being Nat st
( x2 = k & k < card F2() ) ) by A4, A24, A25, A26;
then A27: ( F1(x1) = F1(x2) implies x1 = x2 ) by A3;
F1(x1) = f . x1 by A4, A25;
hence ( not f . x1 = f . x2 or x1 = x2 ) by A4, A26, A27; :: thesis: verum
end;
then A28: dom f, rng f are_equipotent by WELLORD2:def 4;
then reconsider Y = rng f as finite set by A4, CARD_1:38;
A29: card (rng f) = card (card F2()) by A4, A28, CARD_1:5
.= card F2() ;
A30: now :: thesis: for i being Nat holds
( not i >= card F2() or not F1(i) in F2() )
given i being Nat such that A31: i >= card F2() and
A32: F1(i) in F2() ; :: thesis: contradiction
( card F2() < i or card F2() = i ) by A31, XXREAL_0:1;
then A33: F1((card F2())) in F2() by A2, A32;
rng f c= F2() \ {F1((card F2()))}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in F2() \ {F1((card F2()))} )
assume x in rng f ; :: thesis: x in F2() \ {F1((card F2()))}
then consider y being object such that
A34: y in card F2() and
A35: x = f . y by A4, FUNCT_1:def 3;
consider k being Nat such that
A36: y = k and
A37: k < card F2() by A24, A34;
A38: F1(k) = x by A4, A34, A35, A36;
A39: now :: thesis: not x in {F1((card F2()))}
assume x in {F1((card F2()))} ; :: thesis: contradiction
then F1(k) = F1((card F2())) by A38, TARSKI:def 1;
hence contradiction by A3, A37; :: thesis: verum
end;
F1(k) in F2() by A2, A33, A37;
hence x in F2() \ {F1((card F2()))} by A38, A39, XBOOLE_0:def 5; :: thesis: verum
end;
then A40: card Y <= card (F2() \ {F1((card F2()))}) by NAT_1:43;
{F1((card F2()))} c= F2() by A33, ZFMISC_1:31;
then card Y <= (card F2()) - (card {F1((card F2()))}) by A40, CARD_2:44;
then card Y <= (card Y) - 1 by A29, CARD_2:42;
then (card Y) + 1 <= ((card Y) - 1) + 1 by XREAL_1:7;
hence contradiction by NAT_1:13; :: thesis: verum
end;
A41: S1[ 0 ]
proof
assume 0 < card F2() ; :: thesis: F1(0) in F2()
then reconsider X = F2() as non empty set ;
set x = the Element of X;
consider n being Nat such that
A42: the Element of X = F1(n) by A1;
( n = 0 or n > 0 ) ;
hence F1(0) in F2() by A2, A42; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A41, A5);
 hence for n being Nat holds
( F1(n) in F2() iff n < card F2() ) by A30; :: thesis: verum