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
A8: 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
A9: 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
A10: for y being object st y in dom (the_arity_of o) holds
F . y = G . y
proof
let y be object ; :: thesis: ( y in dom (the_arity_of o) implies F . y = G . y )
assume A11: y in dom (the_arity_of o) ; :: thesis: F . y = G . y
then reconsider n = y as Nat by ORDINAL1:def 12;
F . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) by A8, A11;
hence F . y = G . y by A9, A11; :: thesis: verum
end;
A12: dom G = dom (the_arity_of o) by PARTFUN1:def 2;
dom F = dom (the_arity_of o) by PARTFUN1:def 2;
hence F = G by A12, A10, FUNCT_1:2; :: thesis: verum