let F, G be Element of product ((Class R) * (the_arity_of o)); :: thesis: ( ( for n being Nat st n in dom (the_arity_of o) holds
F . n = Class (R . ((the_arity_of o) /. n)),(x . n) ) & ( for n being Nat st n in dom (the_arity_of o) holds
G . n = Class (R . ((the_arity_of o) /. n)),(x . n) ) implies F = G )
assume that
A9: for n being Nat st n in dom (the_arity_of o) holds
F . n = Class (R . ((the_arity_of o) /. n)),(x . n) and
A10: for n being Nat st n in dom (the_arity_of o) holds
G . n = Class (R . ((the_arity_of o) /. n)),(x . n) ; :: thesis: F = G
( dom F = dom ((Class R) * (the_arity_of o)) & dom G = dom ((Class R) * (the_arity_of o)) ) by CARD_3:18;
then A11: ( dom F = dom (the_arity_of o) & dom G = dom (the_arity_of o) ) by PARTFUN1:def 4;
for y being set st y in dom (the_arity_of o) holds
F . y = G . y

proof

let y be set ; :: thesis: ( y in dom (the_arity_of o) implies F . y = G . y )
assume A12: y in dom (the_arity_of o) ; :: thesis: F . y = G . y
then reconsider n = y as Nat by ORDINAL1:def 13;
( F . n = Class (R . ((the_arity_of o) /. n)),(x . n) & G . n = Class (R . ((the_arity_of o) /. n)),(x . n) ) by A9, A10, A12;
hence F . y = G . y ; :: thesis: verum

end;

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