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

proof

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

end;

hence I + J is right-ideal by Def3; :: thesis: verum