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 A1: ( 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 } ) ; :: thesis: x + y in { (a * i) where i is Element of R : i in I }
then consider i being Element of R such that
A2: ( x = a * i & i in I ) ;
consider j being Element of R such that
A3: ( y = a * j & j in I ) by A1;
reconsider k = i + j as Element of R ;
A4: k in I by A2, A3, Def1;
x + y = a * k by A2, A3, VECTSP_1:def 18;
hence x + y in { (a * i) where i is Element of R : i in I } by A4; :: thesis: verum

end;

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