let I be set ; :: thesis: for x1, x2, A, B being ManySortedSet of I st x1 c= A & x2 c= B holds
[|x1,x2|] c= [|A,B|]
let x1, x2, A, 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 object ; :: according to PBOOLE:def 2 :: 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;
x2 . i c= B . i by A2, A3;
then [:(x1 . i),(x2 . i):] c= [:(A . i),(B . i):] by A4, ZFMISC_1:96;
then [|x1,x2|] . i c= [:(A . i),(B . i):] by A3, PBOOLE:def 16;
hence [|x1,x2|] . i c= [|A,B|] . i by A3, PBOOLE:def 16; :: thesis: verum