let H, G be ManySortedFunction of (QuotOSAlg U1,R),U2; :: thesis: ( ( for s being Element of S holds H . s = OSHomQuot F,R,s ) & ( for s being Element of S holds G . s = OSHomQuot F,R,s ) implies H = G )
assume that
A2: for s being Element of S holds H . s = OSHomQuot F,R,s and
A3: for s being Element of S holds G . s = OSHomQuot F,R,s ; :: thesis: H = G

now

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

end;

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