theorem Th5: :: AOFA_I00:5

for N, X, I being non empty set
for v1, v2 being Function st dom v1 = dom v2 & dom v1 = Funcs (X,I) holds
for f being Function of X,N st f is one-to-one & v1 ** (f,N) = v2 ** (f,N) holds
v1 = v2