let H, G be ManySortedFunction of (QuotMSAlg (U1,(MSCng F))),U2; :: thesis: ( ( for s being SortSymbol of S holds H . s = MSHomQuot (F,s) ) & ( for s being SortSymbol of S holds G . s = MSHomQuot (F,s) ) implies H = G )
assume that
A2: for s being SortSymbol of S holds H . s = MSHomQuot (F,s) and
A3: for s being SortSymbol of S holds G . s = MSHomQuot (F,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 = MSHomQuot (F,s) by A2;
hence H . i = G . i by A3; :: thesis: verum

end;

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