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