let A, B be OrderSortedSet of ; :: thesis: ( ( for s being Element of S holds A . s = ParsedTerms X,s ) & ( for s being Element of S holds B . s = ParsedTerms X,s ) implies A = B )
assume that
A8: for s being Element of S holds A . s = ParsedTerms X,s and
A9: for s being Element of S holds B . s = ParsedTerms X,s ; :: thesis: A = B
for i being set st i in the carrier of S holds
A . i = B . i

proof

let i be set ; :: 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 Element of S ;
( A . s = ParsedTerms X,s & B . s = ParsedTerms X,s ) by A8, A9;
hence A . i = B . i ; :: thesis: verum

end;

hence A = B by PBOOLE:3; :: thesis: verum