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 by A1, PARTFUN1:def 4, RELAT_1:def 18;
for x being set st x in dom f holds
f . x is Function

proof

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

end;

then reconsider f = f as ManySortedFunction of by FUNCOP_1:def 6;
for i being set 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)

proof

let i be set ; :: thesis: ( i in the carrier of S implies f . i is Function of (the Sorts of (QuotOSAlg U1,R) . i),(the Sorts of U2 . i) )
assume i in the carrier of S ; :: thesis: f . i is Function of (the Sorts of (QuotOSAlg U1,R) . i),(the Sorts of U2 . i)
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: verum

end;

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