let R be non empty associative well-unital doubleLoopStr ; :: thesis: for I being non empty Subset of R
for a being Element of R holds
( a in sqrt I iff ex n being Element of NAT st a |^ n in sqrt I )
let I be non empty Subset of R; :: thesis: for a being Element of R holds
( a in sqrt I iff ex n being Element of NAT st a |^ n in sqrt I )
let a be Element of R; :: thesis: ( a in sqrt I iff ex n being Element of NAT st a |^ n in sqrt I )

A1: now

assume A2: a in sqrt I ; :: thesis: ex n being Element of NAT st a |^ n in sqrt I
a |^ 1 = a by BINOM:8;
hence ex n being Element of NAT st a |^ n in sqrt I by A2; :: thesis: verum

end;

now

assume ex n being Element of NAT st a |^ n in sqrt I ; :: thesis: a in sqrt I
then consider n being Element of NAT such that
A3: a |^ n in sqrt I ;
consider d being Element of R such that
A4: ( a |^ n = d & ex m being Element of NAT st d |^ m in I ) by A3;
consider m being Element of NAT such that
A5: d |^ m in I by A4;
a |^ (n * m) = d |^ m by A4, BINOM:12;
hence a in sqrt I by A5; :: thesis: verum

end;

hence ( a in sqrt I iff ex n being Element of NAT st a |^ n in sqrt I ) by A1; :: thesis: verum