set ao = the_arity_of o;
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
A8: ( dom f = Args (o,A) & ( for d being Element of Args (o,A) holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
A9: o in the carrier' of S ;
then o in dom (( the Sorts of A #) * the Arity of S) by PARTFUN1:def 2;
then A10: (( the Sorts of A #) * the Arity of S) . o = ( the Sorts of A #) . ( the Arity of S . o) by FUNCT_1:12
.= ( the Sorts of A #) . (the_arity_of o) by MSUALG_1:def 1 ;
A11: for x being object 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 object ; :: thesis:
assume x in ( the Sorts of A #) . (the_arity_of o) ; :: thesis:
then reconsider x1 = x as Element of Args (o,A) by A10, MSUALG_1:def 4;
( f . x1 = R # x1 & ((Class R) #) . (the_arity_of o) = product ((Class R) * (the_arity_of o)) ) by A8, FINSEQ_2:def 5;
hence f . x in ((Class R) #) . (the_arity_of o) ; :: thesis:

end;

o in dom (((Class R) #) * the Arity of S) by A9, PARTFUN1:def 2;
then (((Class R) #) * the Arity of S) . o = ((Class R) #) . ( the Arity of S . o) by FUNCT_1:12
.= ((Class R) #) . (the_arity_of o) by MSUALG_1:def 1 ;
then reconsider f = f as Function of ((( the Sorts of A #) * the Arity of S) . o),((((Class R) #) * the Arity of S) . o) by A8, A10, A11, FUNCT_2:3, MSUALG_1:def 4;
take f ; :: thesis:
thus for x being Element of Args (o,A) holds f . x = R # x by A8; :: thesis: