let f, g be Function of (((the Sorts of A # ) * the Arity of S) . o),((((Class R) # ) * the Arity of S) . o); :: thesis: ( ( for x being Element of Args o,A holds f . x = R # x ) & ( for x being Element of Args o,A holds g . x = R # x ) implies f = g )
assume that
A20: for x being Element of Args o,A holds f . x = R # x and
A21: for x being Element of Args o,A holds g . x = R # 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 A23: ((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 ;
set ao = the_arity_of o;
A24: ( dom f = (the Sorts of A # ) . (the_arity_of o) & dom g = (the Sorts of A # ) . (the_arity_of o) ) by A23, FUNCT_2:def 1;

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 A23, MSUALG_1:def 9;
( f . x1 = R # x1 & g . x1 = R # x1 ) by A20, A21;
hence f . x = g . x ; :: thesis: verum

end;

hence f = g by A24, FUNCT_1:9; :: thesis: verum