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 13;
reconsider f = <*p*> as FinSequence of NAT ;
A1: Product f = p by RVSUM_1:125;
set s = p |^ n;
A2: support (PFactors (p |^ n)) = support (pfexp (p |^ n)) by Def6
.= support (pfexp p) by NAT_3:48
.= {p} by NAT_3:43 ;
A3: f = (PFactors (p |^ n)) * <*p*> by Th47
.= (PFactors (p |^ n)) * (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 Radical (p |^ n) = p by A1, A2, A3, NAT_3:def 5; :: thesis: verum