let F, G be ManySortedFunction of U1,(QuotOSAlg U1,R); :: thesis: ( ( 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
A3: for s being Element of S holds F . s = OSNat_Hom U1,R,s and
A4: for s being Element of S holds G . s = OSNat_Hom U1,R,s ; :: thesis: F = G

now

let i be set ; :: thesis: ( i in the carrier of S implies F . i = G . i )
assume i in the carrier of S ; :: thesis: F . i = G . i
then reconsider s = i as SortSymbol of S ;
( F . s = OSNat_Hom U1,R,s & G . s = OSNat_Hom U1,R,s ) by A3, A4;
hence F . i = G . i ; :: thesis: verum

end;

hence F = G by PBOOLE:3; :: thesis: verum