for P being PNPair
for T being pnptree of P
for t being Node of T
for n being Nat st t ^ <*n*> in dom T holds
T . (t ^ <*n*>) in compn (T . t)