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 :: thesis: for i being object st i in the carrier of S holds
H . i = G . i

let i be object ; :: 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