defpred S1[ Nat, set ] means \$2 = { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . \$1 ) } ;
set n = card F2();
A4: for k being Nat st k in Segm (card F2()) holds
ex x being Subset of (Funcs (F1(),F2())) st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Segm (card F2()) implies ex x being Subset of (Funcs (F1(),F2())) st S1[k,x] )
assume k in Segm (card F2()) ; :: 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 object ; :: 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 ; :: 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
A5: ( dom F = Segm (card F2()) & ( for k being Nat st k in Segm (card F2()) holds
S1[k,F . k] ) ) from A6: 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
A7: i in dom F and
A8: j in dom F and
A9: i <> j ; :: thesis: F . i misses F . j
assume F . i meets F . j ; :: thesis: contradiction
then consider x being object such that
A10: x in (F . i) /\ (F . j) by XBOOLE_0:4;
x in F . i by ;
then x in { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) } by A5, A7;
then A11: ex gi being Function of F1(),F2() st
( x = gi & P1[gi] & gi . F3() = F4() . i ) ;
x in F . j by ;
then x in { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . j ) } by A5, A8;
then A12: ex gj being Function of F1(),F2() st
( x = gj & P1[gj] & gj . F3() = F4() . j ) ;
dom F4() = card F2() by ;
hence contradiction by A1, A5, A7, A8, A9, A11, A12; :: thesis: verum
end;
A13: 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 A14: F . i in rng F by FUNCT_1:def 3;
A15: Funcs (F1(),F2()) is finite by FRAENKEL:6;
thus F . i is finite by ; :: thesis: verum
end;
consider CardF being XFinSequence of NAT such that
A16: dom CardF = dom F and
A17: for i being Nat st i in dom CardF holds
CardF . i = card (F . i) and
A18: card (union (rng F)) = Sum CardF by Lm2, A13, A6;
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 ; :: 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] } ;
A19: { g where g is Function of F1(),F2() : P1[g] } c= union (rng F)
proof
let x be object ; :: 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
A20: x = g and
A21: P1[g] ;
A22: rng F4() = F2() by ;
dom g = F1() by ;
then g . F3() in rng g by ;
then consider y being object such that
A23: y in dom F4() and
A24: F4() . y = g . F3() by ;
F . y = { g1 where g1 is Function of F1(),F2() : ( P1[g1] & g1 . F3() = F4() . y ) } by ;
then A25: g in F . y by ;
F . y in rng F by ;
hence x in union (rng F) by ; :: thesis: verum
end;
union (rng F) c= { g where g is Function of F1(),F2() : P1[g] }
proof
let x be object ; :: 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
A26: x in Y and
A27: Y in rng F by TARSKI:def 4;
consider X being object such that
A28: X in dom F and
A29: F . X = Y by ;
Y = { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . X ) } by A5, A28, A29;
then ex gX being Function of F1(),F2() st
( x = gX & P1[gX] & gX . F3() = F4() . X ) by A26;
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 ; :: 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 A30: 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 A5, A16, A30;
hence CardF . i = card { g where g is Function of F1(),F2() : ( P1[g] & g . F3() = F4() . i ) } by ; :: 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