let X, Y, Z be set ; :: thesis: ( X is finite & X c= [:Y,Z:] implies ex A, B being set st
( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] ) )
deffunc H₂( set ) -> set = $1 `2 ;
assume that
A1: X is finite and
A2: X c= [:Y,Z:] ; :: thesis: ex A, B being set st
( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] )
consider f being Function such that
A3: dom f = X and
A4: for a being set st a in X holds
f . a = H₁(a) from FUNCT_1:sch 3();
consider g being Function such that
A5: dom g = X and
A6: for a being set st a in X holds
g . a = H₂(a) from FUNCT_1:sch 3();
take A = rng f; :: thesis: ex B being set st
( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] )
take B = rng g; :: thesis: ( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] )
thus A is finite by A1, A3, Th26; :: thesis: ( A c= Y & B is finite & B c= Z & X c= [:A,B:] )
thus A c= Y :: thesis: ( B is finite & B c= Z & X c= [:A,B:] )

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in Y )
assume a in A ; :: thesis: a in Y
then consider x being set such that
A7: x in dom f and
A8: f . x = a by FUNCT_1:def 5;
consider y, z being set such that
A9: y in Y and
z in Z and
A10: x = [y,z] by A2, A3, A7, ZFMISC_1:def 2;
f . x = x `1 by A3, A4, A7
.= y by A10, MCART_1:7 ;
hence a in Y by A8, A9; :: thesis: verum

end;

thus B is finite by A1, A5, Th26; :: thesis: ( B c= Z & X c= [:A,B:] )
thus B c= Z :: thesis: X c= [:A,B:]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in Z )
assume a in B ; :: thesis: a in Z
then consider x being set such that
A11: x in dom g and
A12: g . x = a by FUNCT_1:def 5;
consider y, z being set such that
y in Y and
A13: z in Z and
A14: x = [y,z] by A2, A5, A11, ZFMISC_1:def 2;
g . x = x `2 by A5, A6, A11
.= z by A14, MCART_1:7 ;
hence a in Z by A12, A13; :: thesis: verum

end;

thus X c= [:A,B:] :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in [:A,B:] )
assume A15: a in X ; :: thesis: a in [:A,B:]
then consider x, y being set such that
x in Y and
y in Z and
A16: a = [x,y] by A2, ZFMISC_1:def 2;
A17: g . a = a `2 by A6, A15
.= y by A16, MCART_1:7 ;
f . a = a `1 by A4, A15
.= x by A16, MCART_1:7 ;
then A18: x in A by A3, A15, FUNCT_1:def 5;
y in B by A5, A15, A17, FUNCT_1:def 5;
hence a in [:A,B:] by A16, A18, ZFMISC_1:106; :: thesis: verum

end;