set M = { a where a is Element of R : ex n being Element of NAT st a |^ n in I } ;
{ a where a is Element of R : ex n being Element of NAT st a |^ n in I } = sqrt I ;
then reconsider M = { a where a is Element of R : ex n being Element of NAT st a |^ n in I } as non empty Subset of R ;
for y, x being Element of R st x in M holds
y * x in M

proof

let y9, x9 be Element of R; :: thesis: ( x9 in M implies y9 * x9 in M )
reconsider x = x9, y = y9 as Element of R ;
assume x9 in M ; :: thesis: y9 * x9 in M
then consider a being Element of R such that
A1: x = a and
A2: ex n being Element of NAT st a |^ n in I ;
consider n being Element of NAT such that
A3: a |^ n in I by A2;
A4: (y * a) |^ n = (y |^ n) * (a |^ n) by BINOM:9;
(y |^ n) * (a |^ n) in I by A3, Def2;
hence y9 * x9 in M by A1, A4; :: thesis: verum

end;

hence sqrt I is left-ideal ; :: thesis: verum