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
A18: for x being Element of Args o,A holds f . x = R #_os x and
A19: 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 A20: ((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;
A21: ( dom f = (the Sorts of A # ) . (the_arity_of o) & dom g = (the Sorts of A # ) . (the_arity_of o) ) by A20, 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 A20, MSUALG_1:def 9;
( f . x1 = R #_os x1 & g . x1 = R #_os x1 ) by A18, A19;
hence f . x = g . x ; :: thesis: verum

end;

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