let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for M being Subset of V
for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M)
let M be Subset of V; :: thesis: for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M)
let r1, r2 be Real; :: thesis: (r1 + r2) * M c= (r1 * M) + (r2 * M)
for x being VECTOR of V st x in (r1 + r2) * M holds
x in (r1 * M) + (r2 * M)

proof

let x be VECTOR of V; :: thesis: ( x in (r1 + r2) * M implies x in (r1 * M) + (r2 * M) )
assume x in (r1 + r2) * M ; :: thesis: x in (r1 * M) + (r2 * M)
then consider w being VECTOR of V such that
A1: x = (r1 + r2) * w and
A2: w in M ;
A3: r2 * w in { (r2 * u) where u is VECTOR of V : u in M } by A2;
( x = (r1 * w) + (r2 * w) & r1 * w in r1 * M ) by A1, A2, RLVECT_1:def 6;
then x in { (u + v) where u, v is VECTOR of V : ( u in r1 * M & v in r2 * M ) } by A3;
hence x in (r1 * M) + (r2 * M) by RUSUB_4:def 9; :: thesis: verum

end;

hence (r1 + r2) * M c= (r1 * M) + (r2 * M) ; :: thesis: verum