let it1, it2 be NAT * -defined to-naturals homogeneous Function; :: thesis: ( dom it1 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds it1 . p = (p /. i) + 1 ) & dom it2 = n -tuples_on NAT & ( for p being Element of n -tuples_on NAT holds it2 . p = (p /. i) + 1 ) implies it1 = it2 )
assume that
A8: dom it1 = n -tuples_on NAT and
A9: for p being Element of n -tuples_on NAT holds it1 . p = (p /. i) + 1 and
A10: dom it2 = n -tuples_on NAT and
A11: for p being Element of n -tuples_on NAT holds it2 . p = (p /. i) + 1 ; :: thesis: it1 = it2

now

let x be set ; :: thesis: ( x in n -tuples_on NAT implies it1 . x = it2 . x )
assume x in n -tuples_on NAT ; :: thesis: it1 . x = it2 . x
then reconsider x9 = x as Element of n -tuples_on NAT ;
thus it1 . x = (x9 /. i) + 1 by A9
.= it2 . x by A11 ; :: thesis: verum

end;

hence it1 = it2 by A8, A10, FUNCT_1:9; :: thesis: verum