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)

for x being VECTOR of V st x in r * (M1 + M2) holds

x in (r * M1) + (r * M2)

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

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

then A9:
(r * M1) + (r * M2) c= r * (M1 + M2)
;
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;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

for x being VECTOR of V st x in r * (M1 + M2) holds

x in (r * M1) + (r * M2)

proof

then
r * (M1 + M2) c= (r * M1) + (r * M2)
;
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;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

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