defpred S_{1}[ Nat, set ] means $2 = { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . $1 ) } ;

set n = card F_{2}();

A4: for k being Nat st k in Segm (card F_{2}()) holds

ex x being Subset of (Funcs (F_{1}(),F_{2}())) st S_{1}[k,x]
_{1}(),F_{2}())) such that

A5: ( dom F = Segm (card F_{2}()) & ( for k being Nat st k in Segm (card F_{2}()) holds

S_{1}[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

F . i is finite

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 F_{2}() & card { g where g is Function of F_{1}(),F_{2}() : P_{1}[g] } = Sum CardF & ( for i being Nat st i in dom CardF holds

CardF . i = card { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) } ) )

thus dom CardF = card F_{2}()
by A5, A16; :: thesis: ( card { g where g is Function of F_{1}(),F_{2}() : P_{1}[g] } = Sum CardF & ( for i being Nat st i in dom CardF holds

CardF . i = card { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) } ) )

thus card { g where g is Function of F_{1}(),F_{2}() : P_{1}[g] } = Sum CardF
:: thesis: for i being Nat st i in dom CardF holds

CardF . i = card { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) }

CardF . i = card { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) }

CardF . i = card { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) }
; :: thesis: verum

set n = card F

A4: for k being Nat st k in Segm (card F

ex x being Subset of (Funcs (F

proof

consider F being XFinSequence of bool (Funcs (F
let k be Nat; :: thesis: ( k in Segm (card F_{2}()) implies ex x being Subset of (Funcs (F_{1}(),F_{2}())) st S_{1}[k,x] )

assume k in Segm (card F_{2}())
; :: thesis: ex x being Subset of (Funcs (F_{1}(),F_{2}())) st S_{1}[k,x]

set F0 = { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . k ) } ;

{ g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . k ) } c= Funcs (F_{1}(),F_{2}())
_{1}(),F_{2}())) st S_{1}[k,x]
; :: thesis: verum

end;assume k in Segm (card F

set F0 = { g where g is Function of F

{ g where g is Function of F

proof

hence
ex x being Subset of (Funcs (F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . k ) } or x in Funcs (F_{1}(),F_{2}()) )

assume x in { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . k ) }
; :: thesis: x in Funcs (F_{1}(),F_{2}())

then ex g being Function of F_{1}(),F_{2}() st

( x = g & P_{1}[g] & g . F_{3}() = F_{4}() . k )
;

hence x in Funcs (F_{1}(),F_{2}())
by A2, FUNCT_2:8; :: thesis: verum

end;assume x in { g where g is Function of F

then ex g being Function of F

( x = g & P

hence x in Funcs (F

A5: ( dom F = Segm (card F

S

A6: for i, j being Nat st i in dom F & j in dom F & i <> j holds

F . i misses F . j

proof

A13:
for i being Nat st i in dom F holds
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 F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) }
by A5, A7;

then A11: ex gi being Function of F_{1}(),F_{2}() st

( x = gi & P_{1}[gi] & gi . F_{3}() = F_{4}() . i )
;

x in F . j by A10, XBOOLE_0:def 4;

then x in { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . j ) }
by A5, A8;

then A12: ex gj being Function of F_{1}(),F_{2}() st

( x = gj & P_{1}[gj] & gj . F_{3}() = F_{4}() . j )
;

dom F_{4}() = card F_{2}()
by A2, FUNCT_2:def 1;

hence contradiction by A1, A5, A7, A8, A9, A11, A12; :: thesis: verum

end;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 F

then A11: ex gi being Function of F

( x = gi & P

x in F . j by A10, XBOOLE_0:def 4;

then x in { g where g is Function of F

then A12: ex gj being Function of F

( x = gj & P

dom F

hence contradiction by A1, A5, A7, A8, A9, A11, A12; :: thesis: verum

F . i is finite

proof

consider CardF being XFinSequence of NAT such that
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 (F_{1}(),F_{2}()) is finite
by FRAENKEL:6;

thus F . i is finite by A14, A15; :: thesis: verum

end;assume i in dom F ; :: thesis: F . i is finite

then A14: F . i in rng F by FUNCT_1:def 3;

A15: Funcs (F

thus F . i is finite by A14, A15; :: thesis: verum

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 F

CardF . i = card { g where g is Function of F

thus dom CardF = card F

CardF . i = card { g where g is Function of F

thus card { g where g is Function of F

CardF . i = card { g where g is Function of F

proof

for i being Nat st i in dom CardF holds
set G = { g where g is Function of F_{1}(),F_{2}() : P_{1}[g] } ;

A19: { g where g is Function of F_{1}(),F_{2}() : P_{1}[g] } c= union (rng F)
_{1}(),F_{2}() : P_{1}[g] }
_{1}(),F_{2}() : P_{1}[g] } = Sum CardF
by A18, A19, XBOOLE_0:def 10; :: thesis: verum

end;A19: { g where g is Function of F

proof

union (rng F) c= { g where g is Function of F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Function of F_{1}(),F_{2}() : P_{1}[g] } or x in union (rng F) )

assume x in { g where g is Function of F_{1}(),F_{2}() : P_{1}[g] }
; :: thesis: x in union (rng F)

then consider g being Function of F_{1}(),F_{2}() such that

A20: x = g and

A21: P_{1}[g]
;

A22: rng F_{4}() = F_{2}()
by A1, FUNCT_2:def 3;

dom g = F_{1}()
by A2, FUNCT_2:def 1;

then g . F_{3}() in rng g
by A3, FUNCT_1:def 3;

then consider y being object such that

A23: y in dom F_{4}()
and

A24: F_{4}() . y = g . F_{3}()
by A22, FUNCT_1:def 3;

F . y = { g1 where g1 is Function of F_{1}(),F_{2}() : ( P_{1}[g1] & g1 . F_{3}() = F_{4}() . 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;assume x in { g where g is Function of F

then consider g being Function of F

A20: x = g and

A21: P

A22: rng F

dom g = F

then g . F

then consider y being object such that

A23: y in dom F

A24: F

F . y = { g1 where g1 is Function of F

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

proof

hence
card { g where g is Function of F
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 F_{1}(),F_{2}() : P_{1}[g] } )

assume x in union (rng F) ; :: thesis: x in { g where g is Function of F_{1}(),F_{2}() : P_{1}[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 F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . X ) }
by A5, A28, A29;

then ex gX being Function of F_{1}(),F_{2}() st

( x = gX & P_{1}[gX] & gX . F_{3}() = F_{4}() . X )
by A26;

hence x in { g where g is Function of F_{1}(),F_{2}() : P_{1}[g] }
; :: thesis: verum

end;assume x in union (rng F) ; :: thesis: x in { g where g is Function of F

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 F

then ex gX being Function of F

( x = gX & P

hence x in { g where g is Function of F

CardF . i = card { g where g is Function of F

proof

hence
for i being Nat st i in dom CardF holds
let i be Nat; :: thesis: ( i in dom CardF implies CardF . i = card { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) } )

assume A30: i in dom CardF ; :: thesis: CardF . i = card { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) }

F . i = { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) }
by A5, A16, A30;

hence CardF . i = card { g where g is Function of F_{1}(),F_{2}() : ( P_{1}[g] & g . F_{3}() = F_{4}() . i ) }
by A17, A30; :: thesis: verum

end;assume A30: i in dom CardF ; :: thesis: CardF . i = card { g where g is Function of F

F . i = { g where g is Function of F

hence CardF . i = card { g where g is Function of F

CardF . i = card { g where g is Function of F