let F, G be Function of ((((OSClass R) # ) * the Arity of S) . o),(((OSClass R) * the ResultSort of S) . o); :: thesis: ( ( for a being Element of Args o,A st R #_os a in (((OSClass R) # ) * the Arity of S) . o holds
F . (R #_os a) = ((OSQuotRes R,o) * (Den o,A)) . a ) & ( for a being Element of Args o,A st R #_os a in (((OSClass R) # ) * the Arity of S) . o holds
G . (R #_os a) = ((OSQuotRes R,o) * (Den o,A)) . a ) implies F = G )
assume that
A21: for a being Element of Args o,A st R #_os a in (((OSClass R) # ) * the Arity of S) . o holds
F . (R #_os a) = ((OSQuotRes R,o) * (Den o,A)) . a and
A22: for a being Element of Args o,A st R #_os a in (((OSClass R) # ) * the Arity of S) . o holds
G . (R #_os a) = ((OSQuotRes R,o) * (Den o,A)) . a ; :: thesis: F = G
set ao = the_arity_of o;
A23: ( dom the Arity of S = the carrier' of S & rng the Arity of S c= the carrier of S * ) by FUNCT_2:def 1;
then dom (((OSClass R) # ) * the Arity of S) = dom the Arity of S by PARTFUN1:def 4;
then A24: (((OSClass R) # ) * the Arity of S) . o = ((OSClass R) # ) . (the Arity of S . o) by A23, FUNCT_1:22
.= ((OSClass R) # ) . (the_arity_of o) by MSUALG_1:def 6 ;
then A25: ( dom F = ((OSClass R) # ) . (the_arity_of o) & dom G = ((OSClass R) # ) . (the_arity_of o) ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in ((OSClass R) # ) . (the_arity_of o) implies F . x = G . x )
assume A26: x in ((OSClass R) # ) . (the_arity_of o) ; :: thesis: F . x = G . x
then consider a being Element of Args o,A such that
A27: x = R #_os a by A24, Th15;
( F . x = ((OSQuotRes R,o) * (Den o,A)) . a & G . x = ((OSQuotRes R,o) * (Den o,A)) . a ) by A21, A22, A24, A26, A27;
hence F . x = G . x ; :: thesis: verum

end;

hence F = G by A25, FUNCT_1:9; :: thesis: verum