set ao = the_arity_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 2;
then A20: (((Class R) #) * the Arity of S) . o = ((Class R) #) . ( the Arity of S . o) by A19, FUNCT_1:12
.= ((Class R) #) . (the_arity_of o) by MSUALG_1:def 1 ;

A21: now :: thesis: for x being object st x in ((Class R) #) . (the_arity_of o) holds
F . x = G . x

let x be object ; :: 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:2; :: thesis: verum