let I be set ; :: thesis: for x1, x2, A, B being ManySortedSet of I st x1 is V2() & A is V2() & [|x1,A|] = [|x2,B|] holds
( x1 = x2 & A = B )
let x1, x2, A, B be ManySortedSet of I; :: thesis: ( x1 is V2() & A is V2() & [|x1,A|] = [|x2,B|] implies ( x1 = x2 & A = B ) )
assume that
A1: x1 is V2() and
A2: A is V2() and
A3: [|x1,A|] = [|x2,B|] ; :: thesis: ( x1 = x2 & A = B )
now :: thesis: for i being object st i in I holds
x1 . i = x2 . i
let i be object ; :: thesis: ( i in I implies x1 . i = x2 . i )
assume A4: i in I ; :: thesis: x1 . i = x2 . i
then A5: not x1 . i is empty by A1;
A6: not A . i is empty by A2, A4;
[:(x1 . i),(A . i):] = [|x1,A|] . i by A4, PBOOLE:def 16
.= [:(x2 . i),(B . i):] by A3, A4, PBOOLE:def 16 ;
hence x1 . i = x2 . i by A5, A6, ZFMISC_1:110; :: thesis: verum
end;
hence x1 = x2 ; :: thesis: A = B
now :: thesis: for i being object st i in I holds
A . i = B . i
let i be object ; :: thesis: ( i in I implies A . i = B . i )
assume A7: i in I ; :: thesis: A . i = B . i
then A8: not x1 . i is empty by A1;
A9: not A . i is empty by A2, A7;
[:(x1 . i),(A . i):] = [|x1,A|] . i by A7, PBOOLE:def 16
.= [:(x2 . i),(B . i):] by A3, A7, PBOOLE:def 16 ;
hence A . i = B . i by A8, A9, ZFMISC_1:110; :: thesis: verum
end;
hence A = B ; :: thesis: verum