set ao = the_arity_of o;
let f, g be Function of ((( the Sorts of A #) * the Arity of S) . o),((((OSClass R) #) * the Arity of S) . o); :: thesis:
assume that
A12: for x being Element of Args (o,A) holds f . x = R #_os x and
A13: for x being Element of Args (o,A) holds g . x = R #_os x ; :: thesis:
o in the carrier' of S ;
then o in dom (( the Sorts of A #) * the Arity of S) by PARTFUN1:def 2;
then A14: (( 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 ;

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 A14, MSUALG_1:def 4;
f . x1 = R #_os x1 by A12;
hence f . x = g . x by A13; :: thesis:

end;