let a, b be non zero Nat; :: thesis: support (pfexp a) c= support (pfexp (a * b))
set f = pfexp a;
set h = pfexp (a * b);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (pfexp a) or x in support (pfexp (a * b)) )
assume A1: x in support (pfexp a) ; :: thesis: x in support (pfexp (a * b))
then reconsider x = x as Prime by Th34;
A2: (pfexp a) . x = x |-count a by Def8;
(pfexp a) . x <> 0 by A1, PRE_POLY:def 7;
then A3: x divides x |^ (x |-count a) by A2, Th3;
A4: x <> 1 by INT_2:def 4;
then x |^ (x |-count a) divides a by Def7;
then x divides a by A3, NAT_D:4;
then x |^ 1 divides a ;
then A5: x |^ (0 + 1) divides a * b by NAT_D:9;
(pfexp (a * b)) . x = x |-count (a * b) by Def8;
then (pfexp (a * b)) . x <> 0 by A4, A5, Def7;
hence x in support (pfexp (a * b)) by PRE_POLY:def 7; :: thesis: verum