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 y', x' be Element of R; :: thesis: ( x' in M implies y' * x' in M )
assume A1: x' in M ; :: thesis: y' * x' in M
reconsider x = x', y = y' as Element of R ;
consider a being Element of R such that
A2: ( x = a & ex n being Element of NAT st a |^ n in I ) by A1;
consider n being Element of NAT such that
A3: a |^ n in I by A2;
A4: (y |^ n) * (a |^ n) in I by A3, Def2;
(y * a) |^ n = (y |^ n) * (a |^ n) by BINOM:10;
hence y' * x' in M by A2, A4; :: thesis: verum

end;

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