let n be non zero natural number ; :: thesis: Radical n > 0
assume Radical n <= 0 ; :: thesis: contradiction
then Product (PFactors n) = 0 ;
then consider f being FinSequence of COMPLEX such that
A1: ( Product f = 0 & f = (PFactors n) * (canFS (support (PFactors n))) ) by NAT_3:def 5;
for k being Nat holds
( not k in dom f or not f . k = 0 )

proof

A2: rng (canFS (support (PFactors n))) c= support (PFactors n) by FINSEQ_1:def 4;
given k being Nat such that A3: ( k in dom f & f . k = 0 ) ; :: thesis: contradiction
k in dom (canFS (support (PFactors n))) by A1, A3, FUNCT_1:21;
then A4: (canFS (support (PFactors n))) . k in rng (canFS (support (PFactors n))) by FUNCT_1:12;
then (canFS (support (PFactors n))) . k in support (PFactors n) by A2;
then reconsider p = (canFS (support (PFactors n))) . k as prime Element of NAT by NEWTON:def 6;
p in support (PFactors n) by A2, A4;
then A5: p in support (pfexp n) by Def6;
f . k = (PFactors n) . p by A1, A3, FUNCT_1:22
.= p by A5, Def6 ;
hence contradiction by A3; :: thesis: verum

end;

hence contradiction by A1, RVSUM_1:133; :: thesis: verum