defpred S1[ Nat, set ] means $2 = { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . $1 ) } ;
consider n being Nat such that
A4: F2(),n are_equipotent by CARD_1:74;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A5: for k being Nat st k in n holds
ex x being Subset of (Funcs F1(),F2()) st S1[k,x]
proof
let k be Nat; :: thesis: ( k in n implies ex x being Subset of (Funcs F1(),F2()) st S1[k,x] )
assume k in n ; :: thesis: ex x being Subset of (Funcs F1(),F2()) st S1[k,x]
set F0 = { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . k ) } ;
{ g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . k ) } c= Funcs F1(),F2()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . k ) } or x in Funcs F1(),F2() )
assume x in { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . k ) } ; :: thesis: x in Funcs F1(),F2()
then ex g being Function of F1(),F2() st
( x = g & P1[g] & g . F3() = F4() . k ) ;
hence x in Funcs F1(),F2() by A2, FUNCT_2:11; :: thesis: verum
end;
hence ex x being Subset of (Funcs F1(),F2()) st S1[k,x] ; :: thesis: verum
end;
consider F being XFinSequence of bool (Funcs F1(),F2()) such that
A6: ( dom F = n & ( for k being Nat st k in n holds
S1[k,F . k] ) ) from STIRL2_1:sch 5(A5);
 A7: for i, j being Nat st i in dom F & j in dom F & i <> j holds
F . i misses F . j
proof
let i, j be Nat; :: thesis: ( i in dom F & j in dom F & i <> j implies F . i misses F . j )
assume that
A8: i in dom F and
A9: j in dom F and
A10: i <> j ; :: thesis: F . i misses F . j
assume F . i meets F . j ; :: thesis: contradiction
then consider x being set such that
A11: x in (F . i) /\ (F . j) by XBOOLE_0:4;
x in F . i by A11, XBOOLE_0:def 4;
then x in { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) } by A6, A8;
then A12: ex gi being Function of F1(),F2() st
( x = gi & P1[gi] & gi . F3() = F4() . i ) ;
A13: card F2() = card n by A4, CARD_1:21;
A14: card n = n by CARD_1:def 5;
x in F . j by A11, XBOOLE_0:def 4;
then x in { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . j ) } by A6, A9;
then A15: ex gj being Function of F1(),F2() st
( x = gj & P1[gj] & gj . F3() = F4() . j ) ;
dom F4() = card F2() by A2, FUNCT_2:def 1;
hence contradiction by A1, A6, A8, A9, A10, A12, A15, A13, A14, FUNCT_1:def 8; :: thesis: verum
end;
A16: for i being Nat st i in dom F holds
F . i is finite
proof
let i be Nat; :: thesis: ( i in dom F implies F . i is finite )
assume i in dom F ; :: thesis: F . i is finite
then A17: F . i in rng F by FUNCT_1:def 5;
A18: Funcs F1(),F2() is finite by FRAENKEL:16;
rng F c= bool (Funcs F1(),F2()) by RELAT_1:def 19;
hence F . i is finite by A17, A18; :: thesis: verum
end;
consider CardF being XFinSequence of NAT such that
A19: dom CardF = dom F and
A20: for i being Nat st i in dom CardF holds
CardF . i = card (F . i) and
A21: card (union (rng F)) = Sum CardF from STIRL2_1:sch 6(A16, A7);
 take CardF ; :: thesis: ( dom CardF = card F2() & card { g where g is Function of F1(),F2() : P1[g] } = Sum CardF & ( for i being Nat st i in dom CardF holds
CardF . i = card { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) } ) )
thus dom CardF = card F2() by A4, A6, A19, CARD_1:def 5; :: thesis: ( card { g where g is Function of F1(),F2() : P1[g] } = Sum CardF & ( for i being Nat st i in dom CardF holds
CardF . i = card { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) } ) )
thus card { g where g is Function of F1(),F2() : P1[g] } = Sum CardF :: thesis: for i being Nat st i in dom CardF holds
CardF . i = card { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) }
proof
set G = { g where g is Function of F1(),F2() : P1[g] } ;
A22: { g where g is Function of F1(),F2() : P1[g] } c= union (rng F)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of F1(),F2() : P1[g] } or x in union (rng F) )
assume x in { g where g is Function of F1(),F2() : P1[g] } ; :: thesis: x in union (rng F)
then consider g being Function of F1(),F2() such that
A23: x = g and
A24: P1[g] ;
A25: card n = n by CARD_1:def 5;
A26: rng F4() = F2() by A1, FUNCT_2:def 3;
A27: card F2() = card n by A4, CARD_1:21;
dom g = F1() by A2, FUNCT_2:def 1;
then g . F3() in rng g by A3, FUNCT_1:def 5;
then consider y being set such that
A28: y in dom F4() and
A29: F4() . y = g . F3() by A26, FUNCT_1:def 5;
F . y = { g1 where g1 is Function of F1(),F2() : ( P1[g1] & g1 . F3() = F4() . y ) } by A6, A27, A25, A28;
then A30: g in F . y by A24, A29;
F . y in rng F by A6, A28, A27, A25, FUNCT_1:def 5;
hence x in union (rng F) by A23, A30, TARSKI:def 4; :: thesis: verum
end;
union (rng F) c= { g where g is Function of F1(),F2() : P1[g] }
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng F) or x in { g where g is Function of F1(),F2() : P1[g] } )
assume x in union (rng F) ; :: thesis: x in { g where g is Function of F1(),F2() : P1[g] }
then consider Y being set such that
A31: x in Y and
A32: Y in rng F by TARSKI:def 4;
consider X being set such that
A33: X in dom F and
A34: F . X = Y by A32, FUNCT_1:def 5;
Y = { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . X ) } by A6, A33, A34;
then ex gX being Function of F1(),F2() st
( x = gX & P1[gX] & gX . F3() = F4() . X ) by A31;
hence x in { g where g is Function of F1(),F2() : P1[g] } ; :: thesis: verum
end;
hence card { g where g is Function of F1(),F2() : P1[g] } = Sum CardF by A21, A22, XBOOLE_0:def 10; :: thesis: verum
end;
for i being Nat st i in dom CardF holds
CardF . i = card { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) }
proof
let i be Nat; :: thesis: ( i in dom CardF implies CardF . i = card { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) } )
assume A35: i in dom CardF ; :: thesis: CardF . i = card { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) }
F . i = { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) } by A6, A19, A35;
hence CardF . i = card { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) } by A20, A35; :: thesis: verum
end;
hence for i being Nat st i in dom CardF holds
CardF . i = card { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) } ; :: thesis: verum