let A be non degenerated commutative Ring; :: thesis: for I being proper Ideal of A
for x being Element of sqrt I ex m being Nat st
( m in { n where n is Element of NAT : not x |^ n in I } & x |^ (m + 1) in I )
let I be proper Ideal of A; :: thesis: for x being Element of sqrt I ex m being Nat st
( m in { n where n is Element of NAT : not x |^ n in I } & x |^ (m + 1) in I )
let x be Element of sqrt I; :: thesis: ex m being Nat st
( m in { n where n is Element of NAT : not x |^ n in I } & x |^ (m + 1) in I )
set C = { n where n is Element of NAT : not x |^ n in I } ;
x in sqrt I ;
then x in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } by IDEAL_1:def 24;
then consider x1 being Element of A such that
A1: x1 = x and
A2: ex n being Element of NAT st x1 |^ n in I ;
consider n1 being Element of NAT such that
A3: x1 |^ n1 in I by A2;
reconsider n1 = n1 as Element of NAT ;
A4: not n1 in { n where n is Element of NAT : not x |^ n in I }

proof

assume n1 in { n where n is Element of NAT : not x |^ n in I } ; :: thesis: contradiction
then consider n0 being Element of NAT such that
A6: ( n0 = n1 & not x |^ n0 in I ) ;
thus contradiction by A3, A1, A6; :: thesis: verum

end;

assume A7: for m being Nat holds
( not m in { n where n is Element of NAT : not x |^ n in I } or not x |^ (m + 1) in I ) ; :: thesis: contradiction
A8: 0 in { n where n is Element of NAT : not x |^ n in I }

proof

set n = 0 ;
x |^ 0 = 1_ A by BINOM:8
.= 1. A ;
then not x |^ 0 in I by IDEAL_1:19;
hence 0 in { n where n is Element of NAT : not x |^ n in I } ; :: thesis: verum

end;

{ n where n is Element of NAT : not x |^ n in I } = NAT

proof

defpred S₁[ Nat] means $1 in { n where n is Element of NAT : not x |^ n in I } ;
A12: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then not x |^ (n + 1) in I by A7;
hence S₁[n + 1] ; :: thesis: verum

end;

A15: S₁[ 0 ] by A8;
for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A12);
then H: NAT c= { n where n is Element of NAT : not x |^ n in I } ;
{ n where n is Element of NAT : not x |^ n in I } c= NAT

proof

now :: thesis: for o being object st o in { n where n is Element of NAT : not x |^ n in I } holds
o in NAT

let o be object ; :: thesis: ( o in { n where n is Element of NAT : not x |^ n in I } implies o in NAT )
assume o in { n where n is Element of NAT : not x |^ n in I } ; :: thesis: o in NAT
then consider n being Element of NAT such that
I: ( n = o & not x |^ n in I ) ;
thus o in NAT by I; :: thesis: verum

end;

hence { n where n is Element of NAT : not x |^ n in I } c= NAT ; :: thesis: verum

end;

hence { n where n is Element of NAT : not x |^ n in I } = NAT by H; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum