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)

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

hence
(r1 + r2) * M c= (r1 * M) + (r2 * M)
; :: thesis: verum
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;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