set rs = the_result_sort_of o;
set D = the Sorts of A . (the_result_sort_of o);
deffunc H₁( Element of the Sorts of A . (the_result_sort_of o)) -> Element of OSClass R,(the_result_sort_of o) = OSClass R,$1;
consider f being Function such that
A1: ( dom f = the Sorts of A . (the_result_sort_of o) & ( for d being Element of the Sorts of A . (the_result_sort_of o) holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
A2: o in the carrier' of S ;
A3: ( dom the ResultSort of S = the carrier' of S & rng the ResultSort of S c= the carrier of S ) by FUNCT_2:def 1;
o in dom (the Sorts of A * the ResultSort of S) by A2, PARTFUN1:def 4;
then A4: (the Sorts of A * the ResultSort of S) . o = the Sorts of A . (the ResultSort of S . o) by FUNCT_1:22
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def 7 ;
dom ((OSClass R) * the ResultSort of S) = dom the ResultSort of S by A3, PARTFUN1:def 4;
then A5: ((OSClass R) * the ResultSort of S) . o = (OSClass R) . (the ResultSort of S . o) by A3, FUNCT_1:22
.= (OSClass R) . (the_result_sort_of o) by MSUALG_1:def 7 ;
for x being set st x in the Sorts of A . (the_result_sort_of o) holds
f . x in (OSClass R) . (the_result_sort_of o)

proof

let x be set ; :: thesis: ( x in the Sorts of A . (the_result_sort_of o) implies f . x in (OSClass R) . (the_result_sort_of o) )
assume x in the Sorts of A . (the_result_sort_of o) ; :: thesis: f . x in (OSClass R) . (the_result_sort_of o)
then reconsider x1 = x as Element of the Sorts of A . (the_result_sort_of o) ;
f . x1 = OSClass R,x1 by A1;
then f . x1 in OSClass R,(the_result_sort_of o) ;
hence f . x in (OSClass R) . (the_result_sort_of o) by Def13; :: thesis: verum

end;

then reconsider f = f as Function of ((the Sorts of A * the ResultSort of S) . o),(((OSClass R) * the ResultSort of S) . o) by A1, A4, A5, FUNCT_2:5;
take f ; :: thesis: for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass R,x
thus for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = OSClass R,x by A1; :: thesis: verum