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 c= (z1 * M) + (z2 * M)
let M be Subset of V; :: thesis: for z1, z2 being Complex holds (z1 + z2) * M c= (z1 * M) + (z2 * M)
let z1, z2 be Complex; :: thesis: (z1 + z2) * M c= (z1 * M) + (z2 * M)
for x being VECTOR of V st x in (z1 + z2) * M holds
x in (z1 * M) + (z2 * M)

proof

let x be VECTOR of V; :: thesis: ( x in (z1 + z2) * M implies x in (z1 * M) + (z2 * M) )
assume x in (z1 + z2) * M ; :: thesis: x in (z1 * M) + (z2 * M)
then consider w being VECTOR of V such that
A1: x = (z1 + z2) * w and
A2: w in M ;
A3: z2 * w in z2 * M by A2;
( x = (z1 * w) + (z2 * w) & z1 * w in z1 * M ) by A1, A2, CLVECT_1:def 3;
hence x in (z1 * M) + (z2 * M) by A3; :: thesis: verum

end;

hence (z1 + z2) * M c= (z1 * M) + (z2 * M) ; :: thesis: verum