set ao = the_arity_of o;
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
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 4;
then A10: ((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 ;
A11: 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 A10, MSUALG_1:def 9;
( f . x1 = R #_os x1 & ((OSClass R) # ) . (the_arity_of o) = product ((OSClass R) * (the_arity_of o)) ) by A8, PBOOLE:def 19;
hence f . x in ((OSClass R) # ) . (the_arity_of o) ; :: thesis: verum

end;

o in dom (((OSClass R) # ) * the Arity of S) by A9, PARTFUN1:def 4;
then (((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 ;
then reconsider f = f as Function of (((the Sorts of A # ) * the Arity of S) . o),((((OSClass R) # ) * the Arity of S) . o) by A8, A10, A11, 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 A8; :: thesis: verum