set D = Args o,A;
deffunc H₁( Element of Args o,A) -> Element of product ((OSClass R) * (the_arity_of o)) = R #_os $1;
consider f being Function such that
A12: ( dom f = Args o,A & ( for d being Element of Args o,A holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
A14: o in the carrier' of S ;
then o in dom ((the Sorts of A # ) * the Arity of S) by PARTFUN1:def 4;
then A15: ((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 (((OSClass R) # ) * the Arity of S) by A14, PARTFUN1:def 4;
then A16: (((OSClass R) # ) * the Arity of S) . o = ((OSClass R) # ) . (the Arity of S . o) by FUNCT_1:22
.= ((OSClass 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 ((OSClass 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 ((OSClass R) # ) . (the_arity_of o) )
assume x in (the Sorts of A # ) . (the_arity_of o) ; :: thesis: f . x in ((OSClass R) # ) . (the_arity_of o)
then reconsider x1 = x as Element of Args o,A by A15, MSUALG_1:def 9;
A17: f . x1 = R #_os x1 by A12;
((OSClass R) # ) . (the_arity_of o) = product ((OSClass R) * (the_arity_of o)) by PBOOLE:def 19;
hence f . x in ((OSClass R) # ) . (the_arity_of o) by A17; :: thesis: verum

end;

then reconsider f = f as Function of (((the Sorts of A # ) * the Arity of S) . o),((((OSClass R) # ) * the Arity of S) . o) by A12, A15, A16, FUNCT_2:5, MSUALG_1:def 9;
take f ; :: thesis: for x being Element of Args o,A holds f . x = R #_os x
thus for x being Element of Args o,A holds f . x = R #_os x by A12; :: thesis: verum