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

let y9, x9 be Element of R; :: thesis:
reconsider x = x9, y = y9 as Element of R ;
assume x9 in M ; :: thesis:
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:

end;