let A be non degenerated commutative Ring; :: thesis: for p being prime Ideal of A
for n being non zero Nat holds sqrt (p ||^ n) = p
let p be prime Ideal of A; :: thesis: for n being non zero Nat holds sqrt (p ||^ n) = p
let n be non zero Nat; :: thesis: sqrt (p ||^ n) = p
A1: p = sqrt p by TOPZARI1:25, TOPZARI1:20;
defpred S₁[ Nat] means sqrt (p ||^ $1) = p;
A2: S₁[1] by A1, Th8;
A3: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
A5: n > 0 ;
sqrt (p ||^ (n + 1)) = sqrt (p *' (p ||^ n)) by A5, Th10
.= sqrt (p /\ (p ||^ n)) by IDEAL_1:92
.= (sqrt p) /\ (sqrt (p ||^ n)) by Th12
.= p by A1, A4 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for i being non zero Nat holds S₁[i] from NAT_1:sch 10(A2, A3);
hence sqrt (p ||^ n) = p ; :: thesis: verum