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) = (r1 * r2) * M

let M be Subset of V; :: thesis: for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M

let r1, r2 be Real; :: thesis: r1 * (r2 * M) = (r1 * r2) * M

for x being VECTOR of V st x in r1 * (r2 * M) holds

x in (r1 * r2) * M

for x being VECTOR of V st x in (r1 * r2) * M holds

x in r1 * (r2 * M)

hence r1 * (r2 * M) = (r1 * r2) * M by A5; :: thesis: verum

for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M

let M be Subset of V; :: thesis: for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M

let r1, r2 be Real; :: thesis: r1 * (r2 * M) = (r1 * r2) * M

for x being VECTOR of V st x in r1 * (r2 * M) holds

x in (r1 * r2) * M

proof

then A5:
r1 * (r2 * M) c= (r1 * r2) * M
;
let x be VECTOR of V; :: thesis: ( x in r1 * (r2 * M) implies x in (r1 * r2) * M )

assume x in r1 * (r2 * M) ; :: thesis: x in (r1 * r2) * M

then consider w1 being VECTOR of V such that

A1: x = r1 * w1 and

A2: w1 in r2 * M ;

consider w2 being VECTOR of V such that

A3: w1 = r2 * w2 and

A4: w2 in M by A2;

x = (r1 * r2) * w2 by A1, A3, RLVECT_1:def 7;

hence x in (r1 * r2) * M by A4; :: thesis: verum

end;assume x in r1 * (r2 * M) ; :: thesis: x in (r1 * r2) * M

then consider w1 being VECTOR of V such that

A1: x = r1 * w1 and

A2: w1 in r2 * M ;

consider w2 being VECTOR of V such that

A3: w1 = r2 * w2 and

A4: w2 in M by A2;

x = (r1 * r2) * w2 by A1, A3, RLVECT_1:def 7;

hence x in (r1 * r2) * M by A4; :: thesis: verum

for x being VECTOR of V st x in (r1 * r2) * M holds

x in r1 * (r2 * M)

proof

then
(r1 * r2) * M c= r1 * (r2 * M)
;
let x be VECTOR of V; :: thesis: ( x in (r1 * r2) * M implies x in r1 * (r2 * M) )

assume x in (r1 * r2) * M ; :: thesis: x in r1 * (r2 * M)

then consider w1 being VECTOR of V such that

A6: ( x = (r1 * r2) * w1 & w1 in M ) ;

( x = r1 * (r2 * w1) & r2 * w1 in r2 * M ) by A6, RLVECT_1:def 7;

hence x in r1 * (r2 * M) ; :: thesis: verum

end;assume x in (r1 * r2) * M ; :: thesis: x in r1 * (r2 * M)

then consider w1 being VECTOR of V such that

A6: ( x = (r1 * r2) * w1 & w1 in M ) ;

( x = r1 * (r2 * w1) & r2 * w1 in r2 * M ) by A6, RLVECT_1:def 7;

hence x in r1 * (r2 * M) ; :: thesis: verum

hence r1 * (r2 * M) = (r1 * r2) * M by A5; :: thesis: verum