set D = Args o,A;
deffunc H₁( Element of Args o,A) -> Element of product ((Class R) * (the_arity_of o)) = R # $1;
consider f being Function such that
A14: ( dom f = Args o,A & ( for d being Element of Args o,A holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
A15: Args o,A = ((the Sorts of A # ) * the Arity of S) . o by MSUALG_1:def 9;
A16: o in the carrier' of S ;
then o in dom ((the Sorts of A # ) * the Arity of S) by PARTFUN1:def 4;
then A17: ((the Sorts of A # ) * the Arity of S) . o = (the Sorts of A # ) . (the Arity of S . o) by FUNCT_1:22
.= (the Sorts of A # ) . (the_arity_of o) by MSUALG_1:def 6 ;
set ao = the_arity_of o;
o in dom (((Class R) # ) * the Arity of S) by A16, PARTFUN1:def 4;
then A18: (((Class R) # ) * the Arity of S) . o = ((Class R) # ) . (the Arity of S . o) by FUNCT_1:22
.= ((Class R) # ) . (the_arity_of o) by MSUALG_1:def 6 ;
for x being set st x in (the Sorts of A # ) . (the_arity_of o) holds
f . x in ((Class R) # ) . (the_arity_of o)

proof

let x be set ; :: thesis: ( x in (the Sorts of A # ) . (the_arity_of o) implies f . x in ((Class R) # ) . (the_arity_of o) )
assume x in (the Sorts of A # ) . (the_arity_of o) ; :: thesis: f . x in ((Class R) # ) . (the_arity_of o)
then reconsider x1 = x as Element of Args o,A by A17, MSUALG_1:def 9;
A19: f . x1 = R # x1 by A14;
((Class R) # ) . (the_arity_of o) = product ((Class R) * (the_arity_of o)) by PBOOLE:def 19;
hence f . x in ((Class R) # ) . (the_arity_of o) by A19; :: thesis: verum

end;

then reconsider f = f as Function of (((the Sorts of A # ) * the Arity of S) . o),((((Class R) # ) * the Arity of S) . o) by A14, A15, A17, A18, FUNCT_2:5;
take f ; :: thesis: for x being Element of Args o,A holds f . x = R # x
thus for x being Element of Args o,A holds f . x = R # x by A14; :: thesis: verum