let a, n be natural number ; :: thesis: ( a > n & n <> 0 implies (pfexp n) . a = 0 )
assume that
A1: a > n and
A2: n <> 0 ; :: thesis: (pfexp n) . a = 0
reconsider a = a as Element of NAT by ORDINAL1:def 13;

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 4; :: thesis: verum

end;

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

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

end;

end;