deffunc H₁( Element of S) -> Function of ( the Sorts of (QuotOSAlg (U1,R)) . $1),( the Sorts of U2 . $1) = OSHomQuot (F,R,$1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;
for x being object st x in dom f holds
f . x is Function

let x be object ; :: thesis:
assume x in dom f ; :: thesis:
then reconsider y = x as Element of S ;
f . y = OSHomQuot (F,R,y) by A1;
hence f . x is Function ; :: thesis:

end;

then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;
for i being object st i in the carrier of S holds
f . i is Function of ( the Sorts of (QuotOSAlg (U1,R)) . i),( the Sorts of U2 . i)

let i be object ; :: thesis:
assume i in the carrier of S ; :: thesis:
then reconsider s = i as Element of S ;
f . s = OSHomQuot (F,R,s) by A1;
hence f . i is Function of ( the Sorts of (QuotOSAlg (U1,R)) . i),( the Sorts of U2 . i) ; :: thesis:

end;

then reconsider f = f as ManySortedFunction of the Sorts of (QuotOSAlg (U1,R)), the Sorts of U2 by PBOOLE:def 15;
reconsider f = f as ManySortedFunction of (QuotOSAlg (U1,R)),U2 ;
take f ; :: thesis:
thus for s being Element of S holds f . s = OSHomQuot (F,R,s) by A1; :: thesis: