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 that
A8: 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 ) and
A9: 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
( dom F = dom ((OSClass R) * (the_arity_of o)) & dom G = dom ((OSClass R) * (the_arity_of o)) ) by CARD_3:18;
then A10: ( 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 A11: y in dom (the_arity_of o) ; :: thesis: F . y = G . y
then reconsider n = y as Nat ;
consider z being Element of the Sorts of A . ((the_arity_of o) /. n) such that
A12: ( z = x . n & F . n = OSClass R,z ) by A8, A11;
consider z1 being Element of the Sorts of A . ((the_arity_of o) /. n) such that
A13: ( z1 = x . n & G . n = OSClass R,z1 ) by A9, A11;
thus F . y = G . y by A12, A13; :: thesis: verum

end;

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