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