theorem Th35: :: NAT_3:35

for a, n being Nat st a > n & n <> 0 holds
(pfexp n) . a = 0