let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; :: thesis: for M1, M2 being Subset of V
for z being Complex holds z * (M1 + M2) = (z * M1) + (z * M2)
let M1, M2 be Subset of V; :: thesis: for z being Complex holds z * (M1 + M2) = (z * M1) + (z * M2)
let z be Complex; :: thesis: z * (M1 + M2) = (z * M1) + (z * M2)
for x being VECTOR of V st x in (z * M1) + (z * M2) holds
x in z * (M1 + M2)
proof
let x be VECTOR of V; :: thesis: ( x in (z * M1) + (z * M2) implies x in z * (M1 + M2) )
assume x in (z * M1) + (z * M2) ; :: thesis: x in z * (M1 + M2)
then consider w1, w2 being VECTOR of V such that
A1: x = w1 + w2 and
A2: w1 in z * M1 and
A3: w2 in z * M2 ;
consider v2 being VECTOR of V such that
A4: w2 = z * v2 and
A5: v2 in M2 by A3;
consider v1 being VECTOR of V such that
A6: w1 = z * v1 and
A7: v1 in M1 by A2;
A8: v1 + v2 in M1 + M2 by A7, A5;
x = z * (v1 + v2) by A1, A6, A4, CLVECT_1:def 2;
hence x in z * (M1 + M2) by A8; :: thesis: verum
end;
then A9: (z * M1) + (z * M2) c= z * (M1 + M2) ;
for x being VECTOR of V st x in z * (M1 + M2) holds
x in (z * M1) + (z * M2)
proof
let x be VECTOR of V; :: thesis: ( x in z * (M1 + M2) implies x in (z * M1) + (z * M2) )
assume x in z * (M1 + M2) ; :: thesis: x in (z * M1) + (z * M2)
then consider w9 being VECTOR of V such that
A10: x = z * w9 and
A11: w9 in M1 + M2 ;
consider w1, w2 being VECTOR of V such that
A12: w9 = w1 + w2 and
A13: ( w1 in M1 & w2 in M2 ) by A11;
A14: ( z * w1 in z * M1 & z * w2 in z * M2 ) by A13;
x = (z * w1) + (z * w2) by A10, A12, CLVECT_1:def 2;
hence x in (z * M1) + (z * M2) by A14; :: thesis: verum
end;
then z * (M1 + M2) c= (z * M1) + (z * M2) ;
hence z * (M1 + M2) = (z * M1) + (z * M2) by A9, XBOOLE_0:def 10; :: thesis: verum