let A be non degenerated commutative Ring; :: thesis: for M being maximal Ideal of A
for n being non zero Nat holds M ||^ n in PRIMARY (A,M)

let M be maximal Ideal of A; :: thesis: for n being non zero Nat holds M ||^ n in PRIMARY (A,M)
let n be non zero Nat; :: thesis: M ||^ n in PRIMARY (A,M)
reconsider q = M ||^ n as proper Ideal of A by Lm1;
sqrt q is maximal by Th15;
then reconsider Mn = M ||^ n as primary Ideal of A by Th39;
Mn is M -primary by Th15;
hence M ||^ n in PRIMARY (A,M) ; :: thesis: verum