let n be non zero Nat; :: 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 and
A2: 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

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

end;

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