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

proof

let y, x be Element of R; :: thesis: ( x in { (a + b) where a, b is Element of R : ( a in I & b in J ) } implies y * x in { (a + b) where a, b is Element of R : ( a in I & b in J ) } )
assume x in { (a + b) where a, b is Element of R : ( a in I & b in J ) } ; :: thesis: y * x in { (a + b) where a, b is Element of R : ( a in I & b in J ) }
then consider a9, b9 being Element of R such that
A1: x = a9 + b9 and
A2: ( a9 in I & b9 in J ) ;
A3: (y * a9) + (y * b9) = y * x by A1, VECTSP_1:def 2;
( y * a9 in I & y * b9 in J ) by A2, Def2;
hence y * x in { (a + b) where a, b is Element of R : ( a in I & b in J ) } by A3; :: thesis: verum

end;

hence I + J is left-ideal ; :: thesis: verum