let F, G be ManySortedFunction of U1,(QuotMSAlg (U1,R)); :: thesis: ( ( 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) ; :: thesis: F = G

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

let i be object ; :: 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 = MSNat_Hom (U1,R,s) by A2;
hence F . i = G . i by A3; :: thesis: verum

end;

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