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 A2, FUNCT_2:8; :: 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 STIRL2_1:sch 5(A4);
 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 A10, XBOOLE_0:def 4;
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 A10, XBOOLE_0:def 4;
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 A2, FUNCT_2:def 1;
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 A14, A15; :: 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 A5, A16; :: 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 A1, FUNCT_2:def 3;
dom g = F1() by A2, FUNCT_2:def 1;
then g . F3() in rng g by A3, FUNCT_1:def 3;
then consider y being object such that
A23: y in dom F4() and
A24: F4() . y = g . F3() by A22, FUNCT_1:def 3;
F . y = { g1 where g1 is Function of F1(),F2() : ( P1[g1] & g1 . F3() = F4() . y ) } by A5, A23;
then A25: g in F . y by A21, A24;
F . y in rng F by A5, A23, FUNCT_1:def 3;
hence x in union (rng F) by A20, A25, TARSKI:def 4; :: 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 A27, FUNCT_1:def 3;
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 A18, A19, 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 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 A17, A30; :: 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