set D = DTConOSA X;
set F = PTClasses X;
let R1, R2 be MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X; :: thesis: ( ( for i being set st i in the carrier of S holds
R1 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ) & ( for i being set st i in the carrier of S holds
R2 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ) implies R1 = R2 )
assume that
A44: for i being set st i in the carrier of S holds
R1 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } and
A45: for i being set st i in the carrier of S holds
R2 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ; :: thesis: R1 = R2
now :: thesis: for i being object st i in the carrier of S holds
R1 . i = R2 . i
let i be object ; :: thesis: ( i in the carrier of S implies R1 . i = R2 . i )
assume A46: i in the carrier of S ; :: thesis: R1 . i = R2 . i
R1 . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } by A44, A46;
hence R1 . i = R2 . i by A45, A46; :: thesis: verum
end;
hence R1 = R2 ; :: thesis: verum