let R be non empty well-unital associative 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 :: thesis: ( ex n being Element of NAT st a |^ n in sqrt I implies a in sqrt I )
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
A2: a |^ n in sqrt I ;
consider d being Element of R such that
A3: a |^ n = d and
A4: ex m being Element of NAT st d |^ m in I by A2;
consider m being Element of NAT such that
A5: d |^ m in I by A4;
a |^ (n * m) = d |^ m by A3, BINOM:11;
hence a in sqrt I by A5; :: thesis: verum
end;
now :: thesis: ( a in sqrt I implies ex n being Element of NAT st a |^ n in sqrt I )
A6: a |^ 1 = a by BINOM:8;
assume a in sqrt I ; :: thesis: ex n being Element of NAT st a |^ n in sqrt I
hence ex n being Element of NAT st a |^ n in sqrt I by A6; :: 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