let p be Prime; :: thesis: for n being non zero Element of NAT holds Radical (p |^ n) = p
let n be non zero Element of NAT ; :: thesis: Radical (p |^ n) = p
reconsider p = p as prime Element of NAT by ORDINAL1:def 12;
reconsider f = <*p*> as FinSequence of NAT ;
set s = p |^ n;
A1: f = (PFactors (p |^ n)) * <*p*> by Th47
.= (PFactors (p |^ n)) * (canFS {p}) by FINSEQ_1:94 ;
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;
support (PFactors (p |^ n)) = support (pfexp (p |^ n)) by Def6
.= support (pfexp p) by NAT_3:48
.= {p} by NAT_3:43 ;
hence Radical (p |^ n) = p by A1, A2, NAT_3:def 5; :: thesis: verum