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 A1: ( X is finite & 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
A2: dom f = X and
A3: for a being set st a in X holds
f . a = H₁(a) from FUNCT_1:sch 3();
consider g being Function such that
A4: dom g = X and
A5: 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, A2, 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
A6: ( x in dom f & f . x = a ) by FUNCT_1:def 5;
consider y, z being set such that
A7: ( y in Y & z in Z & x = [y,z] ) by A1, A2, A6, ZFMISC_1:def 2;
f . x = x `1 by A2, A3, A6
.= y by A7, MCART_1:7 ;
hence a in Y by A6, A7; :: thesis: verum

end;

thus B is finite by A1, A4, 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
A8: ( x in dom g & g . x = a ) by FUNCT_1:def 5;
consider y, z being set such that
A9: ( y in Y & z in Z & x = [y,z] ) by A1, A4, A8, ZFMISC_1:def 2;
g . x = x `2 by A4, A5, A8
.= z by A9, MCART_1:7 ;
hence a in Z by A8, A9; :: 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 A10: a in X ; :: thesis: a in [:A,B:]
then consider x, y being set such that
A11: ( x in Y & y in Z & a = [x,y] ) by A1, ZFMISC_1:def 2;
A12: g . a = a `2 by A5, A10
.= y by A11, MCART_1:7 ;
f . a = a `1 by A3, A10
.= x by A11, MCART_1:7 ;
then ( x in A & y in B ) by A2, A4, A10, A12, FUNCT_1:def 5;
hence a in [:A,B:] by A11, ZFMISC_1:106; :: thesis: verum

end;