let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X is finite-yielding & X c= [|Y,Z|] holds
ex A, B being ManySortedSet of I st
( A is finite-yielding & A c= Y & B is finite-yielding & B c= Z & X c= [|A,B|] )
let X, Y, Z be ManySortedSet of I; :: thesis: ( X is finite-yielding & X c= [|Y,Z|] implies ex A, B being ManySortedSet of I st
( A is finite-yielding & A c= Y & B is finite-yielding & B c= Z & X c= [|A,B|] ) )
assume that
A1: X is finite-yielding and
A2: X c= [|Y,Z|] ; :: thesis: ex A, B being ManySortedSet of I st
( A is finite-yielding & A c= Y & B is finite-yielding & B c= Z & X c= [|A,B|] )
defpred S₁[ object , object ] means ex D, b being set st
( D = $2 & D is finite & D c= Y . $1 & b is finite & b c= Z . $1 & X . $1 c= [:D,b:] );
A3: for i being object st i in I holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in I implies ex j being object st S₁[i,j] )
assume A4: i in I ; :: thesis: ex j being object st S₁[i,j]
then X . i c= [|Y,Z|] . i by A2;
then A5: X . i c= [:(Y . i),(Z . i):] by A4, PBOOLE:def 16;
X . i is finite by A1;
then consider A, B being set such that
A6: ( A is finite & A c= Y . i & B is finite & B c= Z . i & X . i c= [:A,B:] ) by A5, FINSET_1:13;
thus ex j being object st S₁[i,j] by A6; :: thesis: verum

end;

consider A being ManySortedSet of I such that
A7: for i being object st i in I holds
S₁[i,A . i] from PBOOLE:sch 3(A3);
defpred S₂[ object , object ] means ex D being set st
( D = $2 & A . $1 is finite & A . $1 c= Y . $1 & D is finite & D c= Z . $1 & X . $1 c= [:(A . $1),D:] );
A8: for i being object st i in I holds
ex j being object st S₂[i,j]

proof

let i be object ; :: thesis: ( i in I implies ex j being object st S₂[i,j] )
assume i in I ; :: thesis: ex j being object st S₂[i,j]
then S₁[i,A . i] by A7;
hence ex j being object st S₂[i,j] ; :: thesis: verum

end;

consider B being ManySortedSet of I such that
A9: for i being object st i in I holds
S₂[i,B . i] from PBOOLE:sch 3(A8);
take A ; :: thesis: ex B being ManySortedSet of I st
( A is finite-yielding & A c= Y & B is finite-yielding & B c= Z & X c= [|A,B|] )
take B ; :: thesis: ( A is finite-yielding & A c= Y & B is finite-yielding & B c= Z & X c= [|A,B|] )
thus A is finite-yielding :: thesis: ( A c= Y & B is finite-yielding & B c= Z & X c= [|A,B|] )

proof

let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or A . i is finite )
assume i in I ; :: thesis: A . i is finite
then S₂[i,B . i] by A9;
hence A . i is finite ; :: thesis: verum

end;

thus A c= Y :: thesis: ( B is finite-yielding & B c= Z & X c= [|A,B|] )

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or A . i c= Y . i )
assume i in I ; :: thesis: A . i c= Y . i
then S₂[i,B . i] by A9;
hence A . i c= Y . i ; :: thesis: verum

end;

thus B is finite-yielding :: thesis: ( B c= Z & X c= [|A,B|] )

proof

let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or B . i is finite )
assume i in I ; :: thesis: B . i is finite
then S₂[i,B . i] by A9;
hence B . i is finite ; :: thesis: verum

end;

thus B c= Z :: thesis: X c= [|A,B|]

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or B . i c= Z . i )
assume i in I ; :: thesis: B . i c= Z . i
then S₂[i,B . i] by A9;
hence B . i c= Z . i ; :: thesis: verum

end;

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

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or X . i c= [|A,B|] . i )
assume A10: i in I ; :: thesis: X . i c= [|A,B|] . i
then S₂[i,B . i] by A9;
then X . i c= [:(A . i),(B . i):] ;
hence X . i c= [|A,B|] . i by A10, PBOOLE:def 16; :: thesis: verum

end;