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

proof

let x be VECTOR of V; :: thesis: ( x in (r * M1) + (r * M2) implies x in r * (M1 + M2) )
assume x in (r * M1) + (r * M2) ; :: thesis: x in r * (M1 + M2)
then x in { (u + v) where u, v is VECTOR of V : ( u in r * M1 & v in r * M2 ) } by RUSUB_4:def 9;
then consider w1, w2 being VECTOR of V such that
A1: x = w1 + w2 and
A2: w1 in r * M1 and
A3: w2 in r * M2 ;
consider v2 being VECTOR of V such that
A4: w2 = r * v2 and
A5: v2 in M2 by A3;
consider v1 being VECTOR of V such that
A6: w1 = r * v1 and
A7: v1 in M1 by A2;
v1 + v2 in { (u + v) where u, v is VECTOR of V : ( u in M1 & v in M2 ) } by A7, A5;
then A8: v1 + v2 in M1 + M2 by RUSUB_4:def 9;
x = r * (v1 + v2) by A1, A6, A4, RLVECT_1:def 5;
hence x in r * (M1 + M2) by A8; :: thesis: verum

end;

then A9: (r * M1) + (r * M2) c= r * (M1 + M2) ;
for x being VECTOR of V st x in r * (M1 + M2) holds
x in (r * M1) + (r * M2)

proof

let x be VECTOR of V; :: thesis: ( x in r * (M1 + M2) implies x in (r * M1) + (r * M2) )
assume x in r * (M1 + M2) ; :: thesis: x in (r * M1) + (r * M2)
then consider w9 being VECTOR of V such that
A10: x = r * w9 and
A11: w9 in M1 + M2 ;
w9 in { (u + v) where u, v is VECTOR of V : ( u in M1 & v in M2 ) } by A11, RUSUB_4:def 9;
then consider w1, w2 being VECTOR of V such that
A12: w9 = w1 + w2 and
A13: ( w1 in M1 & w2 in M2 ) ;
A14: ( r * w1 in r * M1 & r * w2 in { (r * w) where w is VECTOR of V : w in M2 } ) by A13;
x = (r * w1) + (r * w2) by A10, A12, RLVECT_1:def 5;
then x in { (u + v) where u, v is VECTOR of V : ( u in r * M1 & v in r * M2 ) } by A14;
hence x in (r * M1) + (r * M2) by RUSUB_4:def 9; :: thesis: verum

end;

then r * (M1 + M2) c= (r * M1) + (r * M2) ;
hence r * (M1 + M2) = (r * M1) + (r * M2) by A9; :: thesis: verum