let a, b be non zero Nat; :: thesis: support (pfexp (a * b)) = (support (pfexp a)) \/ (support (pfexp b))
set f = pfexp a;
set g = pfexp b;
set h = pfexp (a * b);
thus support (pfexp (a * b)) c= (support (pfexp a)) \/ (support (pfexp b)) :: according to XBOOLE_0:def 10 :: thesis: (support (pfexp a)) \/ (support (pfexp b)) c= support (pfexp (a * b))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (pfexp (a * b)) or x in (support (pfexp a)) \/ (support (pfexp b)) )
assume A1: x in support (pfexp (a * b)) ; :: thesis: x in (support (pfexp a)) \/ (support (pfexp b))
then reconsider x = x as Prime by Th34;
A2: (pfexp (a * b)) . x <> 0 by A1, PRE_POLY:def 7;
A3: x <> 1 by INT_2:def 4;
A4: ( (pfexp (a * b)) . x = x |-count (a * b) & x |^ (x |-count (a * b)) = (x |^ (x |-count a)) * (x |^ (x |-count b)) ) by Def8, Th29;

per cases ( x divides x |^ (x |-count a) or x divides x |^ (x |-count b) ) by A2, A4, Th3, NEWTON:80;

suppose x divides x |^ (x |-count a) ; :: thesis: x in (support (pfexp a)) \/ (support (pfexp b))

then x divides a by A3, Th26;
then (pfexp a) . x <> 0 by Th38;
then x in support (pfexp a) by PRE_POLY:def 7;
hence x in (support (pfexp a)) \/ (support (pfexp b)) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x divides x |^ (x |-count b) ; :: thesis: x in (support (pfexp a)) \/ (support (pfexp b))

then x divides b by A3, Th26;
then (pfexp b) . x <> 0 by Th38;
then x in support (pfexp b) by PRE_POLY:def 7;
hence x in (support (pfexp a)) \/ (support (pfexp b)) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

( support (pfexp a) c= support (pfexp (a * b)) & support (pfexp b) c= support (pfexp (a * b)) ) by Th45;
hence (support (pfexp a)) \/ (support (pfexp b)) c= support (pfexp (a * b)) by XBOOLE_1:8; :: thesis: verum