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
A6: dom it1 = n -tuples_on NAT and
A7: for p being Element of n -tuples_on NAT holds it1 . p = (p . i) + 1 and
A8: dom it2 = n -tuples_on NAT and
A9: for p being Element of n -tuples_on NAT holds it2 . p = (p . i) + 1 ; :: thesis: it1 = it2

now :: thesis: for x being object st x in n -tuples_on NAT holds
it1 . x = it2 . x

let x be object ; :: 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 A7
.= it2 . x by A9 ; :: thesis: verum

end;

hence it1 = it2 by A6, A8; :: thesis: verum