let q be Prime; :: thesis: for g being Element of NAT st g <> 0 holds
ex p1 being bag of SetPrimes st
( p1 = (SetPrimes --> 0) +* (q,g) & support p1 = {q} & Product p1 = g )
let g be Element of NAT ; :: thesis: ( g <> 0 implies ex p1 being bag of SetPrimes st
( p1 = (SetPrimes --> 0) +* (q,g) & support p1 = {q} & Product p1 = g ) )
set p = (SetPrimes --> 0) +* (q,g);
reconsider p = (SetPrimes --> 0) +* (q,g) as ManySortedSet of SetPrimes ;
A1: dom (SetPrimes --> 0) = SetPrimes by FUNCOP_1:13;
then q in dom (SetPrimes --> 0) by NEWTON:def 6;
then A2: p . q = g by FUNCT_7:31;
A3: for x being set st not x in {q} holds
p . x = 0

proof

let x be set ; :: thesis: ( not x in {q} implies p . x = 0 )
assume not x in {q} ; :: thesis: p . x = 0
then x <> q by TARSKI:def 1;
hence p . x = 0 by Lm1; :: thesis: verum

end;

now

let z be set ; :: thesis: ( z in support p & not z in {q} implies z in {q} )
assume A4: z in support p ; :: thesis: ( not z in {q} implies z in {q} )
z in dom p

proof

assume not z in dom p ; :: thesis: contradiction
then p . z = {} by FUNCT_1:def 2;
hence contradiction by A4, PRE_POLY:def 7; :: thesis: verum

end;

then reconsider y = z as Element of SetPrimes by A1, FUNCT_7:30;
assume not z in {q} ; :: thesis: z in {q}
p . y <> 0 by A4, PRE_POLY:def 7;
hence z in {q} by A3; :: thesis: verum

end;

then for z being set st z in support p holds
z in {q} ;
then A5: support p c= {q} by TARSKI:def 3;
assume A6: g <> 0 ; :: thesis: ex p1 being bag of SetPrimes st
( p1 = (SetPrimes --> 0) +* (q,g) & support p1 = {q} & Product p1 = g )

now

let z be set ; :: thesis: ( z in {q} implies z in support p )
assume z in {q} ; :: thesis: z in support p
then A7: z = q by TARSKI:def 1;
thus z in support p by A6, A2, A7, PRE_POLY:def 7; :: thesis: verum

end;

then A8: {q} c= support p by TARSKI:def 3;
then A9: support p = {q} by A5, XBOOLE_0:def 10;
reconsider p = p as bag of SetPrimes by A5, PRE_POLY:def 8;
A10: q in support p by A9, TARSKI:def 1;
A11: q in dom p

proof

assume not q in dom p ; :: thesis: contradiction
then p . q = {} by FUNCT_1:def 2;
hence contradiction by A10, PRE_POLY:def 7; :: thesis: verum

end;

take p ; :: thesis: ( p = (SetPrimes --> 0) +* (q,g) & support p = {q} & Product p = g )
consider f being FinSequence of COMPLEX such that
A12: Product p = Product f and
A13: f = p * (canFS (support p)) by NAT_3:def 5;
f = p * <*q*> by A9, A13, UPROOTS:4;
then f = <*(p . q)*> by A11, FINSEQ_2:34;
hence ( p = (SetPrimes --> 0) +* (q,g) & support p = {q} & Product p = g ) by A2, A5, A8, A12, RVSUM_1:95, XBOOLE_0:def 10; :: thesis: verum