let I be set ; :: thesis: for X, Z, Y being ManySortedSet of I st X is locally-finite & Z is locally-finite & X c= [|Y,Z|] holds
ex A being ManySortedSet of I st
( A is locally-finite & A c= Y & X c= [|A,Z|] )
let X, Z, Y be ManySortedSet of I; :: thesis: ( X is locally-finite & Z is locally-finite & X c= [|Y,Z|] implies ex A being ManySortedSet of I st
( A is locally-finite & A c= Y & X c= [|A,Z|] ) )
assume that
A1: X is locally-finite and
A2: Z is locally-finite and
A3: X c= [|Y,Z|] ; :: thesis: ex A being ManySortedSet of I st
( A is locally-finite & A c= Y & X c= [|A,Z|] )
defpred S₁[ set , set ] means ( $2 is finite & $2 c= Y . $1 & X . $1 c= [:$2,(Z . $1):] );
A4: 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 A5: i in I ; :: thesis: ex j being set st S₁[i,j]
then A6: X . i is finite by A1, PRE_CIRC:def 3;
A7: Z . i is finite by A2, A5, PRE_CIRC:def 3;
X . i c= [|Y,Z|] . i by A3, A5, PBOOLE:def 5;
then X . i c= [:(Y . i),(Z . i):] by A5, PBOOLE:def 21;
then consider A' being set such that
A8: ( A' is finite & A' c= Y . i & X . i c= [:A',(Z . i):] ) by A6, A7, FINSET_1:33;
take A' ; :: thesis: S₁[i,A']
thus ( A' is finite & A' c= Y . i & X . i c= [:A',(Z . i):] ) by A8; :: thesis: verum

end;

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

proof

let i be set ; :: according to PRE_CIRC:def 3 :: 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: X c= [|A,Z|]

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 X c= [|A,Z|] :: thesis: verum

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or X . i c= [|A,Z|] . i )
assume A10: i in I ; :: thesis: X . i c= [|A,Z|] . i
then X . i c= [:(A . i),(Z . i):] by A9;
hence X . i c= [|A,Z|] . i by A10, PBOOLE:def 21; :: thesis: verum

end;