defpred S1[ Nat, set ] means $2 = card (F2() . $1);
A3: for k being Nat st k in len F2() holds
ex x being Element of NAT st S1[k,x]
proof
let k be Nat; :: thesis: ( k in len F2() implies ex x being Element of NAT st S1[k,x] )
assume k in len F2() ; :: thesis: ex x being Element of NAT st S1[k,x]
then consider m being Nat such that
A4: F2() . k,m are_equipotent by A1, CARD_1:74;
card (F2() . k) = card m by A4, CARD_1:21;
hence ex x being Element of NAT st S1[k,x] ; :: thesis: verum
end;
consider CardF being XFinSequence of NAT such that
A5: ( dom CardF = len F2() & ( for k being Nat st k in len F2() holds
S1[k,CardF . k] ) ) from STIRL2_1:sch 5(A3);
 take CardF ; :: thesis: ( dom CardF = dom F2() & ( for i being Nat st i in dom CardF holds
CardF . i = card (F2() . i) ) & card (union (rng F2())) = Sum CardF )
thus dom CardF = dom F2() by A5; :: thesis: ( ( for i being Nat st i in dom CardF holds
CardF . i = card (F2() . i) ) & card (union (rng F2())) = Sum CardF )
thus for i being Nat st i in dom CardF holds
CardF . i = card (F2() . i) by A5; :: thesis: card (union (rng F2())) = Sum CardF
H: addnat "**" CardF = Sum CardF by AFINSQ_2:63;
per cases ( len CardF = 0 or len CardF <> 0 ) ;
suppose A6: len CardF = 0 ; :: thesis: card (union (rng F2())) = Sum CardF
then union (rng F2()) is empty by A5, RELAT_1:65, ZFMISC_1:2;
hence card (union (rng F2())) = Sum CardF by A6, AFINSQ_2:def 9, BINOP_2:5, H; :: thesis: verum
end;
suppose A7: len CardF <> 0 ; :: thesis: card (union (rng F2())) = Sum CardF
then consider f being Function of NAT ,NAT such that
A8: f . 0 = CardF . 0 and
A9: for n being Nat st n + 1 < len CardF holds
f . (n + 1) = addnat . (f . n),(CardF . (n + 1)) and
A10: addnat "**" CardF = f . ((len CardF) - 1) by AFINSQ_2:def 9;
defpred S2[ Nat] means ( $1 < len CardF implies ( card (union (rng (F2() | ($1 + 1)))) = f . $1 & union (rng (F2() | ($1 + 1))) is finite ) );
A11: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A12: S2[k] ; :: thesis: S2[k + 1]
set k1 = k + 1;
set Fk1 = F2() | (k + 1);
set rFk1 = rng (F2() | (k + 1));
assume A13: k + 1 < len CardF ; :: thesis: ( card (union (rng (F2() | ((k + 1) + 1)))) = f . (k + 1) & union (rng (F2() | ((k + 1) + 1))) is finite )
reconsider urFk1 = union (rng (F2() | (k + 1))) as finite set by A12, A13, NAT_1:13;
A14: f . (k + 1) = addnat . (f . k),(CardF . (k + 1)) by A9, A13;
A15: union (rng (F2() | (k + 1))) misses F2() . (k + 1)
proof
assume union (rng (F2() | (k + 1))) meets F2() . (k + 1) ; :: thesis: contradiction
then consider x being set such that
A16: x in (union (rng (F2() | (k + 1)))) /\ (F2() . (k + 1)) by XBOOLE_0:4;
A17: x in F2() . (k + 1) by A16, XBOOLE_0:def 4;
A18: k + 1 in dom F2() by A5, A13, NAT_1:45;
x in union (rng (F2() | (k + 1))) by A16, XBOOLE_0:def 4;
then consider Y being set such that
A19: x in Y and
A20: Y in rng (F2() | (k + 1)) by TARSKI:def 4;
consider X being set such that
A21: X in dom (F2() | (k + 1)) and
A22: (F2() | (k + 1)) . X = Y by A20, FUNCT_1:def 5;
reconsider X = X as Element of NAT by A21;
A23: (F2() | (k + 1)) . X = F2() . X by A21, FUNCT_1:70;
A24: X in (dom F2()) /\ (k + 1) by A21, RELAT_1:90;
then X in k + 1 by XBOOLE_0:def 4;
then A25: X <> k + 1 ;
X in dom F2() by A24, XBOOLE_0:def 4;
then Y misses F2() . (k + 1) by A2, A22, A18, A25, A23;
hence contradiction by A19, A17, XBOOLE_0:3; :: thesis: verum
end;
k + 1 in dom F2() by A5, A13, NAT_1:45;
then reconsider Fk1 = F2() . (k + 1) as finite set by A1;
k + 1 in len F2() by A5, A13, NAT_1:45;
then card Fk1 = CardF . (k + 1) by A5;
then A26: f . (k + 1) = (f . k) + (card Fk1) by A14, BINOP_2:def 23;
card (urFk1 \/ Fk1) = (f . k) + (card Fk1) by A12, A13, A15, CARD_2:53, NAT_1:13;
hence ( card (union (rng (F2() | ((k + 1) + 1)))) = f . (k + 1) & union (rng (F2() | ((k + 1) + 1))) is finite ) by A26, Th54; :: thesis: verum
set rFk2 = rng (F2() | ((k + 1) + 1));
end;
reconsider C1 = (len CardF) - 1 as Element of NAT by A7, NAT_1:20;
A27: C1 < C1 + 1 by NAT_1:13;
A28: F2() | (len CardF) = F2() by A5, RELAT_1:97;
A29: S2[ 0 ]
proof
assume 0 < len CardF ; :: thesis: ( card (union (rng (F2() | (0 + 1)))) = f . 0 & union (rng (F2() | (0 + 1))) is finite )
A30: union (rng (F2() | (0 + 1))) = (union (rng (F2() | 0 ))) \/ (F2() . 0 ) by Th54;
0 in len CardF by A7, NAT_1:45;
hence ( card (union (rng (F2() | (0 + 1)))) = f . 0 & union (rng (F2() | (0 + 1))) is finite ) by A1, A5, A8, A30, ZFMISC_1:2; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(A29, A11);
hence card (union (rng F2())) = Sum CardF by A10, A27, A28, H; :: thesis: verum
end;
end;