theorem Th58: :: NUMPOLY1:58

for n, k being Nat holds NPower (n,(k + 1)) = (NPower (n,k)) ^ <*((k + 1) |^ n)*>