for Z1 being Tree
for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1
for w being Element of Z1 | p st v = p ^ w holds
succ v, succ w are_equipotent