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 ;
dom (SetPrimes --> 0) = SetPrimes by FUNCOP_1:13;
then q in dom (SetPrimes --> 0) by NEWTON:def 6;
then A1: p . q = g by FUNCT_7:31;
A2: for x being object st not x in {q} holds
p . x = 0
proof
let x be object ; :: 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 :: thesis: for z being set st z in support p & not z in {q} holds
z in {q}
let z be set ; :: thesis: ( z in support p & not z in {q} implies z in {q} )
assume A3: 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 A3, PRE_POLY:def 7; :: thesis: verum
end;
then reconsider y = z as Element of SetPrimes ;
assume not z in {q} ; :: thesis: z in {q}
p . y <> 0 by A3, PRE_POLY:def 7;
hence z in {q} by A2; :: thesis: verum
end;
then for z being object st z in support p holds
z in {q} ;
then A4: support p c= {q} ;
assume A5: g <> 0 ; :: thesis: ex p1 being bag of SetPrimes st
( p1 = (SetPrimes --> 0) +* (q,g) & support p1 = {q} & Product p1 = g )
now :: thesis: for z being object st z in {q} holds
z in support p
let z be object ; :: thesis: ( z in {q} implies z in support p )
assume z in {q} ; :: thesis: z in support p
then A6: z = q by TARSKI:def 1;
thus z in support p by A5, A1, A6, PRE_POLY:def 7; :: thesis: verum
end;
then A7: {q} c= support p ;
then A8: support p = {q} by A4, XBOOLE_0:def 10;
reconsider p = p as bag of SetPrimes by A4, PRE_POLY:def 8;
A9: q in support p by A8, TARSKI:def 1;
A10: q in dom p
proof
assume not q in dom p ; :: thesis: contradiction
then p . q = {} by FUNCT_1:def 2;
hence contradiction by A9, 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
A11: Product p = Product f and
A12: f = p * (canFS (support p)) by NAT_3:def 5;
f = p * <*q*> by A8, A12, FINSEQ_1:94;
then f = <*(p . q)*> by A10, FINSEQ_2:34;
hence ( p = (SetPrimes --> 0) +* (q,g) & support p = {q} & Product p = g ) by A1, A4, A7, A11, RVSUM_1:95, XBOOLE_0:def 10; :: thesis: verum