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 13;
reconsider f = <*p*> as FinSequence of NAT ;
A2: Product f = p by RVSUM_1:125;
A3: f = (PFactors p) * <*p*> by Th46
.= (PFactors p) * (canFS {p}) by UPROOTS:6 ;
rng f c= NAT by FINSEQ_1:def 4;
then rng f c= COMPLEX by NUMBERS:20, XBOOLE_1:1;
then f is FinSequence of COMPLEX by FINSEQ_1:def 4;
hence p = Radical p by A1, A2, A3, NAT_3:def 5; :: thesis: verum