set M = { (a * i) where i is Element of R : i in I } ;
for x, y being Element of R st x in { (a * i) where i is Element of R : i in I } & y in { (a * i) where i is Element of R : i in I } holds
x + y in { (a * i) where i is Element of R : i in I }

proof

let x, y be Element of R; :: thesis: ( x in { (a * i) where i is Element of R : i in I } & y in { (a * i) where i is Element of R : i in I } implies x + y in { (a * i) where i is Element of R : i in I } )
assume that
A1: x in { (a * i) where i is Element of R : i in I } and
A2: y in { (a * i) where i is Element of R : i in I } ; :: thesis: x + y in { (a * i) where i is Element of R : i in I }
consider i being Element of R such that
A3: ( x = a * i & i in I ) by A1;
consider j being Element of R such that
A4: ( y = a * j & j in I ) by A2;
reconsider k = i + j as Element of R ;
( k in I & x + y = a * k ) by A3, A4, Def1, VECTSP_1:def 7;
hence x + y in { (a * i) where i is Element of R : i in I } ; :: thesis: verum

end;

hence a * I is add-closed ; :: thesis: verum