let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; :: thesis: for M being Subset of V
for z1, z2 being Complex holds z1 * (z2 * M) = (z1 * z2) * M
let M be Subset of V; :: thesis: for z1, z2 being Complex holds z1 * (z2 * M) = (z1 * z2) * M
let z1, z2 be Complex; :: thesis: z1 * (z2 * M) = (z1 * z2) * M
for x being VECTOR of V st x in z1 * (z2 * M) holds
x in (z1 * z2) * M
proof
let x be VECTOR of V; :: thesis: ( x in z1 * (z2 * M) implies x in (z1 * z2) * M )
assume x in z1 * (z2 * M) ; :: thesis: x in (z1 * z2) * M
then consider w1 being VECTOR of V such that
A1: x = z1 * w1 and
A2: w1 in z2 * M ;
consider w2 being VECTOR of V such that
A3: w1 = z2 * w2 and
A4: w2 in M by A2;
x = (z1 * z2) * w2 by A1, A3, CLVECT_1:def 4;
hence x in (z1 * z2) * M by A4; :: thesis: verum
end;
then A5: z1 * (z2 * M) c= (z1 * z2) * M ;
for x being VECTOR of V st x in (z1 * z2) * M holds
x in z1 * (z2 * M)
proof
let x be VECTOR of V; :: thesis: ( x in (z1 * z2) * M implies x in z1 * (z2 * M) )
assume x in (z1 * z2) * M ; :: thesis: x in z1 * (z2 * M)
then consider w1 being VECTOR of V such that
A6: ( x = (z1 * z2) * w1 & w1 in M ) ;
( x = z1 * (z2 * w1) & z2 * w1 in z2 * M ) by A6, CLVECT_1:def 4;
hence x in z1 * (z2 * M) ; :: thesis: verum
end;
then (z1 * z2) * M c= z1 * (z2 * M) ;
hence z1 * (z2 * M) = (z1 * z2) * M by A5, XBOOLE_0:def 10; :: thesis: verum