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
proof
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;
then A5: r1 * (r2 * M) c= (r1 * r2) * M ;
for x being VECTOR of V st x in (r1 * r2) * M holds
x in r1 * (r2 * M)
proof
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;
then (r1 * r2) * M c= r1 * (r2 * M) ;
hence r1 * (r2 * M) = (r1 * r2) * M by A5; :: thesis: verum