let X, Y be ManySortedSet of I; :: thesis: ( ( for i being set st i in I holds
ex P being RelStr st
( P = C . i & X . i = the InternalRel of P ) ) & ( for i being set st i in I holds
ex P being RelStr st
( P = C . i & Y . i = the InternalRel of P ) ) implies X = Y )
assume that
A5: for j being set st j in I holds
ex R being RelStr st
( R = C . j & X . j = the InternalRel of R ) and
A6: for j being set st j in I holds
ex R being RelStr st
( R = C . j & Y . j = the InternalRel of R ) ; :: thesis: X = Y
for i being object st i in I holds
X . i = Y . i

proof

let i be object ; :: thesis: ( i in I implies X . i = Y . i )
assume A7: i in I ; :: thesis: X . i = Y . i
then A8: ex R being RelStr st
( R = C . i & X . i = the InternalRel of R ) by A5;
ex R being RelStr st
( R = C . i & Y . i = the InternalRel of R ) by A6, A7;
hence X . i = Y . i by A8; :: thesis: verum

end;

hence X = Y by PBOOLE:3; :: thesis: verum