let F, G be ManySortedFunction of U1,(QuotMSAlg (U1,R)); ( ( for s being SortSymbol of S holds F . s = MSNat_Hom (U1,R,s) ) & ( for s being SortSymbol of S holds G . s = MSNat_Hom (U1,R,s) ) implies F = G )
assume that
A2:
for s being SortSymbol of S holds F . s = MSNat_Hom (U1,R,s)
and
A3:
for s being SortSymbol of S holds G . s = MSNat_Hom (U1,R,s)
; F = G
hence
F = G
by PBOOLE:3; verum