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); ( ( 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
; 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 for x being object st x in ((Class R) #) . (the_arity_of o) holds
F . x = G . xlet x be
object ;
( x in ((Class R) #) . (the_arity_of o) implies F . x = G . x )assume A22:
x in ((Class R) #) . (the_arity_of o)
;
F . x = G . xthen 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;
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; verum