let a, n be Nat; :: thesis: ( a > n & n <> 0 implies (pfexp n) . a = 0 )
assume A1: ( a > n & n <> 0 ) ; :: thesis: (pfexp n) . a = 0
reconsider a = a as Element of NAT by ORDINAL1:def 12;

per cases ( not a is prime or a is prime ) ;

suppose not a is prime ; :: thesis: (pfexp n) . a = 0

then not a in dom (pfexp n) by Th33;
hence (pfexp n) . a = 0 by FUNCT_1:def 2; :: thesis: verum

end;

suppose A2: a is prime ; :: thesis: (pfexp n) . a = 0

then a <> 1 ;
then a |-count n = 0 by A1, Th23;
hence (pfexp n) . a = 0 by A2, Def8; :: thesis: verum

end;

end;