let p be Prime; :: thesis: p = Radical p
A1: support (PFactors p) = support (pfexp p) by Def6
.= {p} by NAT_3:43 ;
reconsider p = p as prime Element of NAT by ORDINAL1:def 12;
reconsider f = <*p*> as FinSequence of NAT ;
rng f c= NAT by FINSEQ_1:def 4;
then rng f c= COMPLEX by NUMBERS:20;
then A2: ( Product f = p & f is FinSequence of COMPLEX ) by FINSEQ_1:def 4, RVSUM_1:95;
f = (PFactors p) * <*p*> by Th46
.= (PFactors p) * (canFS {p}) by FINSEQ_1:94 ;
hence p = Radical p by A1, A2, NAT_3:def 5; :: thesis: verum