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