let F, G be Element of product ((OSClass R) * (the_arity_of o)); :: thesis: ( ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & F . n = OSClass (R,y) ) ) & ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & G . n = OSClass (R,y) ) ) implies F = G )
assume A7: ( ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & F . n = OSClass (R,y) ) ) & ( for n being Nat st n in dom (the_arity_of o) holds
ex y being Element of the Sorts of A . ((the_arity_of o) /. n) st
( y = x . n & G . n = OSClass (R,y) ) ) ) ; :: thesis: F = G
A8: 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 A9: y in dom (the_arity_of o) ; :: thesis: F . y = G . y
then reconsider n = y as Nat ;
( ex z being Element of the Sorts of A . ((the_arity_of o) /. n) st
( z = x . n & F . n = OSClass (R,z) ) & ex z1 being Element of the Sorts of A . ((the_arity_of o) /. n) st
( z1 = x . n & G . n = OSClass (R,z1) ) ) by A7, A9;
hence F . y = G . y ; :: thesis: verum

end;

A10: 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 A10, A8, FUNCT_1:2; :: thesis: verum