let I be set ; :: thesis: for X, Y, Z being ManySortedSet of st X is finite-yielding & X c= [|Y,Z|] holds
ex A, B being ManySortedSet of 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 ; :: thesis: ( X is finite-yielding & X c= [|Y,Z|] implies ex A, B being ManySortedSet of 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 st
( A is finite-yielding & A c= Y & B is finite-yielding & B c= Z & X c= [|A,B|] )
defpred S₁[ set , set ] means ex b being set st
( $2 is finite & $2 c= Y . $1 & b is finite & b c= Z . $1 & X . $1 c= [:$2,b:] );
A3: for i being set st i in I holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in I implies ex j being set st S₁[i,j] )
assume A4: i in I ; :: thesis: ex j being set st S₁[i,j]
then A5: X . i is finite by A1, LL1;
X . i c= [|Y,Z|] . i by A2, A4, PBOOLE:def 5;
then X . i c= [:(Y . i),(Z . i):] by A4, PBOOLE:def 21;
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:32;
thus ex j being set st S₁[i,j] by A6; :: thesis: verum

end;

consider A being ManySortedSet of such that
A7: for i being set st i in I holds
S₁[i,A . i] from PBOOLE:sch 3(A3);
defpred S₂[ set , set ] means ( A . $1 is finite & A . $1 c= Y . $1 & $2 is finite & $2 c= Z . $1 & X . $1 c= [:(A . $1),$2:] );
A8: for i being set st i in I holds
ex j being set st S₂[i,j] by A7;
consider B being ManySortedSet of such that
A9: for i being set st i in I holds
S₂[i,B . i] from PBOOLE:sch 3(A8);
take A ; :: thesis: ex B being ManySortedSet of 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 set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or A . i is finite )
assume i in I ; :: thesis: A . i is finite
hence A . i is finite by A9; :: thesis: verum

end;

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

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or A . i c= Y . i )
assume i in I ; :: thesis: A . i c= Y . i
hence A . i c= Y . i by A9; :: thesis: verum

end;

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

proof

let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or B . i is finite )
assume i in I ; :: thesis: B . i is finite
hence B . i is finite by A9; :: thesis: verum

end;

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

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or B . i c= Z . i )
assume i in I ; :: thesis: B . i c= Z . i
hence B . i c= Z . i by A9; :: thesis: verum

end;

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

proof

let i be set ; :: according to PBOOLE:def 5 :: 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 X . i c= [:(A . i),(B . i):] by A9;
hence X . i c= [|A,B|] . i by A10, PBOOLE:def 21; :: thesis: verum

end;