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 x, y being Element of R st x in M & y in M holds
x + y in M

proof

let x, y be Element of R; :: thesis: ( x in M & y in M implies x + y in M )
assume that
A1: x in M and
A2: y in M ; :: thesis: x + y in M
consider a being Element of R such that
A3: x = a and
A4: ex n being Element of NAT st a |^ n in I by A1;
consider n being Element of NAT such that
A5: a |^ n in I by A4;
consider b being Element of R such that
A6: y = b and
A7: ex m being Element of NAT st b |^ m in I by A2;
consider m being Element of NAT such that
A8: b |^ m in I by A7;
set p = (a,b) In_Power (n + m);
consider f being sequence of the carrier of R such that
A9: Sum ((a,b) In_Power (n + m)) = f . (len ((a,b) In_Power (n + m))) and
A10: f . 0 = 0. R and
A11: for j being Nat
for v being Element of R st j < len ((a,b) In_Power (n + m)) & v = ((a,b) In_Power (n + m)) . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred S₁[ Element of NAT ] means f . R in I;
A12: for i being Element of NAT st 1 <= i & i <= len ((a,b) In_Power (n + m)) holds
((a,b) In_Power (n + m)) . i in I

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len ((a,b) In_Power (n + m)) implies ((a,b) In_Power (n + m)) . i in I )
assume that
A13: 1 <= i and
A14: i <= len ((a,b) In_Power (n + m)) ; :: thesis: ((a,b) In_Power (n + m)) . i in I
set r = i - 1;
set l = (n + m) - (i - 1);
1 - 1 <= i - 1 by A13, XREAL_1:9;
then reconsider r = i - 1 as Element of NAT by INT_1:3;
i <= (n + m) + 1 by A14, BINOM:def 7;
then r <= ((n + m) + 1) - 1 by XREAL_1:9;
then r - r <= (n + m) - r by XREAL_1:9;
then reconsider l = (n + m) - (i - 1) as Element of NAT by INT_1:3;
i in Seg (len ((a,b) In_Power (n + m))) by A13, A14, FINSEQ_1:1;
then A15: i in dom ((a,b) In_Power (n + m)) by FINSEQ_1:def 3;
then A16: ((a,b) In_Power (n + m)) . i = ((a,b) In_Power (n + m)) /. i by PARTFUN1:def 6
.= (((n + m) choose r) * (a |^ l)) * (b |^ r) by A15, BINOM:def 7 ;

per cases ( n <= l or l < n ) ;

suppose n <= l ; :: thesis: ((a,b) In_Power (n + m)) . i in I

then consider k being Nat such that
A17: l = n + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
a |^ l = (a |^ n) * (a |^ k) by A17, BINOM:10;
then a |^ l in I by A5, Def3;
then ((n + m) choose r) * (a |^ l) in I by Th17;
hence ((a,b) In_Power (n + m)) . i in I by A16, Def3; :: thesis: verum

end;

suppose l < n ; :: thesis: ((a,b) In_Power (n + m)) . i in I

then ((n + m) + (- r)) + r < n + r by XREAL_1:6;
then (- n) + (n + m) < (- n) + (n + r) by XREAL_1:6;
then consider k being Nat such that
A18: r = m + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
b |^ r = (b |^ m) * (b |^ k) by A18, BINOM:10;
then b |^ r in I by A8, Def3;
hence ((a,b) In_Power (n + m)) . i in I by A16, Def3; :: thesis: verum

end;

end;

end;

A19: now :: thesis: for j being Element of NAT st 0 <= j & j < len ((a,b) In_Power (n + m)) & S₁[j] holds
S₁[j + 1]

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len ((a,b) In_Power (n + m)) & S₁[j] implies S₁[j + 1] )
assume that
0 <= j and
A20: j < len ((a,b) In_Power (n + m)) ; :: thesis: ( S₁[j] implies S₁[j + 1] )
thus ( S₁[j] implies S₁[j + 1] ) :: thesis: verum

proof

assume A21: f . j in I ; :: thesis: S₁[j + 1]
A22: j + 1 <= len ((a,b) In_Power (n + m)) by A20, NAT_1:13;
1 <= j + 1 by NAT_1:11;
then j + 1 in Seg (len ((a,b) In_Power (n + m))) by A22, FINSEQ_1:1;
then j + 1 in dom ((a,b) In_Power (n + m)) by FINSEQ_1:def 3;
then A23: ((a,b) In_Power (n + m)) /. (j + 1) = ((a,b) In_Power (n + m)) . (j + 1) by PARTFUN1:def 6;
then A24: ((a,b) In_Power (n + m)) /. (j + 1) in I by A12, A22, NAT_1:11;
f . (j + 1) = (f . j) + (((a,b) In_Power (n + m)) /. (j + 1)) by A11, A20, A23;
hence S₁[j + 1] by A21, A24, Def1; :: thesis: verum

end;

end;

A25: (a + b) |^ (n + m) = Sum ((a,b) In_Power (n + m)) by BINOM:25;
A26: S₁[ 0 ] by A10, Th2;
for i being Element of NAT st 0 <= i & i <= len ((a,b) In_Power (n + m)) holds
S₁[i] from INT_1:sch 7(A26, A19);
then (a + b) |^ (n + m) in I by A25, A9;
hence x + y in M by A3, A6; :: thesis: verum

end;

hence sqrt I is add-closed ; :: thesis: verum