set ao = the_arity_of o;
set ro = the_result_sort_of o;
let F, G be Function of ((((Class R) # ) * the Arity of S) . o),(((Class R) * the ResultSort of S) . o); :: thesis: ( ( for a being Element of Args o,A st R # a in (((Class R) # ) * the Arity of S) . o holds
F . (R # a) = ((QuotRes R,o) * (Den o,A)) . a ) & ( for a being Element of Args o,A st R # a in (((Class R) # ) * the Arity of S) . o holds
G . (R # a) = ((QuotRes R,o) * (Den o,A)) . a ) implies F = G )
assume that
A17: for a being Element of Args o,A st R # a in (((Class R) # ) * the Arity of S) . o holds
F . (R # a) = ((QuotRes R,o) * (Den o,A)) . a and
A18: for a being Element of Args o,A st R # a in (((Class R) # ) * the Arity of S) . o holds
G . (R # a) = ((QuotRes R,o) * (Den o,A)) . a ; :: thesis: F = G
A19: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then dom (((Class R) # ) * the Arity of S) = dom the Arity of S by PARTFUN1:def 4;
then A20: (((Class R) # ) * the Arity of S) . o = ((Class R) # ) . (the Arity of S . o) by A19, FUNCT_1:22
.= ((Class R) # ) . (the_arity_of o) by MSUALG_1:def 6 ;

A21: now

let x be set ; :: thesis: ( x in ((Class R) # ) . (the_arity_of o) implies F . x = G . x )
assume A22: x in ((Class R) # ) . (the_arity_of o) ; :: thesis: F . x = G . x
then consider a being Element of Args o,A such that
A23: x = R # a by A20, Th2;
F . x = ((QuotRes R,o) * (Den o,A)) . a by A17, A20, A22, A23;
hence F . x = G . x by A18, A20, A22, A23; :: thesis: verum

end;

( dom F = ((Class R) # ) . (the_arity_of o) & dom G = ((Class R) # ) . (the_arity_of o) ) by A20, FUNCT_2:def 1;
hence F = G by A21, FUNCT_1:9; :: thesis: verum