let C1, C2 be MSCongruence of U1; :: thesis: ( ( for s being SortSymbol of S holds C1 . s = MSCng (F,s) ) & ( for s being SortSymbol of S holds C2 . s = MSCng (F,s) ) implies C1 = C2 )
assume that
A18: for s being SortSymbol of S holds C1 . s = MSCng (F,s) and
A19: for s being SortSymbol of S holds C2 . s = MSCng (F,s) ; :: thesis: C1 = C2

now :: thesis: for i being object st i in the carrier of S holds
C1 . i = C2 . i

let i be object ; :: thesis: ( i in the carrier of S implies C1 . i = C2 . i )
assume i in the carrier of S ; :: thesis: C1 . i = C2 . i
then reconsider s = i as Element of S ;
C1 . s = MSCng (F,s) by A18;
hence C1 . i = C2 . i by A19; :: thesis: verum

end;

hence C1 = C2 by PBOOLE:3; :: thesis: verum