let a, b be non zero Nat; :: thesis: support (pfexp a) = support (pfexp (a |^ b))
set f = pfexp a;
set g = pfexp (a |^ b);
a |^ b = (a |^ (b -' 1)) * a by PEPIN:26;
hence support (pfexp a) c= support (pfexp (a |^ b)) by Th45; :: according to XBOOLE_0:def 10 :: thesis: support (pfexp (a |^ b)) c= support (pfexp a)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (pfexp (a |^ b)) or x in support (pfexp a) )
assume A1: x in support (pfexp (a |^ b)) ; :: thesis: x in support (pfexp a)
then reconsider x = x as Prime by Th34;
A2: ( (pfexp (a |^ b)) . x = x |-count (a |^ b) & x <> 1 ) by Def8, INT_2:def 4;
(pfexp (a |^ b)) . x <> 0 by A1, PRE_POLY:def 7;
then x divides a |^ b by A2, Th27;
then (pfexp a) . x <> 0 by Th5, Th38;
hence x in support (pfexp a) by PRE_POLY:def 7; :: thesis: verum