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 that
A1: x1 c= A and
A2: 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 A3: i in I ; :: thesis: [|x1,x2|] . i c= [|A,B|] . i
then A4: x1 . i c= A . i by A1, PBOOLE:def 5;
x2 . i c= B . i by A2, A3, PBOOLE:def 5;
then [:(x1 . i),(x2 . i):] c= [:(A . i),(B . i):] by A4, ZFMISC_1:119;
then [|x1,x2|] . i c= [:(A . i),(B . i):] by A3, PBOOLE:def 21;
hence [|x1,x2|] . i c= [|A,B|] . i by A3, PBOOLE:def 21; :: thesis: verum