let V be non empty RealLinearSpace-like 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 + 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 w' being VECTOR of V such that
A1: ( x = r * w' & w' in M1 + M2 ) ;
w' in { (u + v) where u, v is VECTOR of V : ( u in M1 & v in M2 ) } by A1, RUSUB_4:def 10;
then consider w1, w2 being VECTOR of V such that
A2: ( w' = w1 + w2 & w1 in M1 & w2 in M2 ) ;
A3: x = (r * w1) + (r * w2) by A1, A2, RLVECT_1:def 9;
A4: r * w1 in r * M1 by A2;
r * w2 in { (r * w) where w is VECTOR of V : w in M2 } by A2;
then x in { (u + v) where u, v is VECTOR of V : ( u in r * M1 & v in r * M2 ) } by A3, A4;
hence x in (r * M1) + (r * M2) by RUSUB_4:def 10; :: thesis: verum

end;

then A5: r * (M1 + M2) c= (r * M1) + (r * M2) by SUBSET_1:7;
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 10;
then consider w1, w2 being VECTOR of V such that
A6: ( x = w1 + w2 & w1 in r * M1 & w2 in r * M2 ) ;
consider v1 being VECTOR of V such that
A7: ( w1 = r * v1 & v1 in M1 ) by A6;
consider v2 being VECTOR of V such that
A8: ( w2 = r * v2 & v2 in M2 ) by A6;
A9: x = r * (v1 + v2) by A6, A7, A8, RLVECT_1:def 9;
v1 + v2 in { (u + v) where u, v is VECTOR of V : ( u in M1 & v in M2 ) } by A7, A8;
then v1 + v2 in M1 + M2 by RUSUB_4:def 10;
hence x in r * (M1 + M2) by A9; :: thesis: verum

end;

then (r * M1) + (r * M2) c= r * (M1 + M2) by SUBSET_1:7;
hence r * (M1 + M2) = (r * M1) + (r * M2) by A5, XBOOLE_0:def 10; :: thesis: verum