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
A20: 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
A21: 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
set ao = the_arity_of o;
set ro = the_result_sort_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 (((Class R) # ) * the Arity of S) = dom the Arity of S by PARTFUN1:def 4;
then A24: (((Class R) # ) * the Arity of S) . o = ((Class R) # ) . (the Arity of S . o) by A23, FUNCT_1:22
.= ((Class R) # ) . (the_arity_of o) by MSUALG_1:def 6 ;
A27: ( dom F = ((Class R) # ) . (the_arity_of o) & dom G = ((Class R) # ) . (the_arity_of o) ) by A24, FUNCT_2:def 1;

now

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

end;

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