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 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 ((OSClass R) #) . (the_arity_of o)

proof

let x be object ; :: 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 4;
( f . x1 = R #_os x1 & ((OSClass R) #) . (the_arity_of o) = product ((OSClass R) * (the_arity_of o)) ) by A8, FINSEQ_2:def 5;
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 2;
then (((OSClass R) #) * the Arity of S) . o = ((OSClass R) #) . ( the Arity of S . o) by FUNCT_1:12
.= ((OSClass 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),((((OSClass R) #) * the Arity of S) . o) by A8, A10, A11, FUNCT_2:3, MSUALG_1:def 4;
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