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)) -> Subset of ( the Sorts of A . (the_result_sort_of o)) = Class (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: for x being object st x in the Sorts of A . (the_result_sort_of o) holds
f . x in (Class R) . (the_result_sort_of o)

proof

let x be object ; :: thesis: ( x in the Sorts of A . (the_result_sort_of o) implies f . x in (Class R) . (the_result_sort_of o) )
assume x in the Sorts of A . (the_result_sort_of o) ; :: thesis: f . x in (Class R) . (the_result_sort_of o)
then reconsider x1 = x as Element of the Sorts of A . (the_result_sort_of o) ;
f . x1 = Class (R,x1) by A1;
then f . x1 in Class (R . (the_result_sort_of o)) by EQREL_1:def 3;
hence f . x in (Class R) . (the_result_sort_of o) by Def6; :: thesis: verum

end;

o in the carrier' of S ;
then o in dom ( the Sorts of A * the ResultSort of S) by PARTFUN1:def 2;
then A3: ( the Sorts of A * the ResultSort of S) . o = the Sorts of A . ( the ResultSort of S . o) by FUNCT_1:12
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def 2 ;
A4: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then dom ((Class R) * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def 2;
then ((Class R) * the ResultSort of S) . o = (Class R) . ( the ResultSort of S . o) by A4, FUNCT_1:12
.= (Class R) . (the_result_sort_of o) by MSUALG_1:def 2 ;
then reconsider f = f as Function of (( the Sorts of A * the ResultSort of S) . o),(((Class R) * the ResultSort of S) . o) by A1, A3, A2, FUNCT_2:3;
take f ; :: thesis: for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = Class (R,x)
thus for x being Element of the Sorts of A . (the_result_sort_of o) holds f . x = Class (R,x) by A1; :: thesis: verum