let I be set ; :: thesis: for x1, A, x2, B being ManySortedSet of I st x1 c= A & x2 c= B holds
[|x1,x2|] c= [|A,B|]
let x1, A, x2, B be ManySortedSet of I; :: thesis: ( x1 c= A & x2 c= B implies [|x1,x2|] c= [|A,B|] )
assume A1: ( x1 c= A & x2 c= B ) ; :: thesis: [|x1,x2|] c= [|A,B|]
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or [|x1,x2|] . i c= [|A,B|] . i )
assume A2: i in I ; :: thesis: [|x1,x2|] . i c= [|A,B|] . i
then ( x1 . i c= A . i & x2 . i c= B . i ) by A1, PBOOLE:def 5;
then [:(x1 . i),(x2 . i):] c= [:(A . i),(B . i):] by ZFMISC_1:119;
then [|x1,x2|] . i c= [:(A . i),(B . i):] by A2, PBOOLE:def 21;
hence [|x1,x2|] . i c= [|A,B|] . i by A2, PBOOLE:def 21; :: thesis: verum