let A, B be ManySortedSet of the carrier of S; :: thesis: ( ( for s being SortSymbol of S holds A . s = FreeSort (X,s) ) & ( for s being SortSymbol of S holds B . s = FreeSort (X,s) ) implies A = B )

assume that

A2: for s being SortSymbol of S holds A . s = FreeSort (X,s) and

A3: for s being SortSymbol of S holds B . s = FreeSort (X,s) ; :: thesis: A = B

for i being object st i in the carrier of S holds

A . i = B . i

assume that

A2: for s being SortSymbol of S holds A . s = FreeSort (X,s) and

A3: for s being SortSymbol of S holds B . s = FreeSort (X,s) ; :: thesis: A = B

for i being object st i in the carrier of S holds

A . i = B . i

proof

hence
A = B
; :: thesis: verum
let i be object ; :: thesis: ( i in the carrier of S implies A . i = B . i )

assume i in the carrier of S ; :: thesis: A . i = B . i

then reconsider s = i as SortSymbol of S ;

A . s = FreeSort (X,s) by A2;

hence A . i = B . i by A3; :: thesis: verum

end;assume i in the carrier of S ; :: thesis: A . i = B . i

then reconsider s = i as SortSymbol of S ;

A . s = FreeSort (X,s) by A2;

hence A . i = B . i by A3; :: thesis: verum