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 4;
then A14: ((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 ;

A15: now

let x be set ; :: 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 9;
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:9; :: thesis: verum