let I be set ; :: thesis: for A, x1, x2 being ManySortedSet of st ( A = [0] I or A = {x1} or A = {x2} or A = {x1,x2} ) holds
A c= {x1,x2}
let A, x1, x2 be ManySortedSet of ; :: thesis: ( ( A = [0] I or A = {x1} or A = {x2} or A = {x1,x2} ) implies A c= {x1,x2} )
assume A1: ( A = [0] I or A = {x1} or A = {x2} or A = {x1,x2} ) ; :: thesis: A c= {x1,x2}
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or A . i c= {x1,x2} . i )
assume A2: i in I ; :: thesis: A . i c= {x1,x2} . i

per cases ( A = [0] I or A = {x1} or A = {x2} or A = {x1,x2} ) by A1;

suppose A = [0] I ; :: thesis: A . i c= {x1,x2} . i

then A . i = {} by PBOOLE:5;
then A . i c= {(x1 . i),(x2 . i)} by ZFMISC_1:42;
hence A . i c= {x1,x2} . i by A2, Def2; :: thesis: verum

end;

suppose A = {x1} ; :: thesis: A . i c= {x1,x2} . i

then A . i = {(x1 . i)} by A2, Def1;
then A . i c= {(x1 . i),(x2 . i)} by ZFMISC_1:42;
hence A . i c= {x1,x2} . i by A2, Def2; :: thesis: verum

end;

suppose A = {x2} ; :: thesis: A . i c= {x1,x2} . i

then A . i = {(x2 . i)} by A2, Def1;
then A . i c= {(x1 . i),(x2 . i)} by ZFMISC_1:42;
hence A . i c= {x1,x2} . i by A2, Def2; :: thesis: verum

end;

suppose A = {x1,x2} ; :: thesis: A . i c= {x1,x2} . i

hence A . i c= {x1,x2} . i ; :: thesis: verum

end;

end;