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: ( ( for x being Element of Args (o,A) holds f . x = R #_os x ) & ( for x being Element of Args (o,A) holds g . x = R #_os x ) implies f = g )
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: f = g
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 ;

A15: now :: thesis: for x being object st x in ( the Sorts of A #) . (the_arity_of o) holds
f . x = g . x

let x be object ; :: thesis: ( x in ( the Sorts of A #) . (the_arity_of o) implies f . x = g . x )
assume x in ( the Sorts of A #) . (the_arity_of o) ; :: thesis: f . x = g . x
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: verum

end;

( dom f = ( the Sorts of A #) . (the_arity_of o) & dom g = ( the Sorts of A #) . (the_arity_of o) ) by A14, FUNCT_2:def 1;
hence f = g by A15, FUNCT_1:2; :: thesis: verum