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 being ManySortedSet of I st
( A is finite-yielding & A c= Y & X c= [|A,Z|] )
let X, Y, Z be ManySortedSet of I; :: thesis: ( X is finite-yielding & X c= [|Y,Z|] implies ex A being ManySortedSet of I st
( A is finite-yielding & A c= Y & X c= [|A,Z|] ) )
assume that
A1: X is finite-yielding and
A2: X c= [|Y,Z|] ; :: thesis: ex A being ManySortedSet of I st
( A is finite-yielding & A c= Y & X c= [|A,Z|] )
defpred S₁[ object , object ] means ex D being set st
( D = $2 & D is finite & D c= Y . $1 & X . $1 c= [:D,(Z . $1):] );
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 A9 being set such that
A6: ( A9 is finite & A9 c= Y . i & X . i c= [:A9,(Z . i):] ) by A5, FINSET_1:14;
take A9 ; :: thesis: S₁[i,A9]
thus S₁[i,A9] 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);
take A ; :: thesis: ( A is finite-yielding & A c= Y & X c= [|A,Z|] )
thus A is finite-yielding :: thesis: ( A c= Y & X c= [|A,Z|] )

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,A . i] by A7;
hence A . i is finite ; :: thesis: verum

end;

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

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,A . i] by A7;
hence A . i c= Y . i ; :: thesis: verum

end;

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

proof

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

end;