let V be non empty CLSStruct ; :: thesis: for M, N being Subset of V
for z being Complex st M c= N holds
z * M c= z * N
let M, N be Subset of V; :: thesis: for z being Complex st M c= N holds
z * M c= z * N
let z be Complex; :: thesis: ( M c= N implies z * M c= z * N )
assume A1: M c= N ; :: thesis: z * M c= z * N

now :: thesis: for x being VECTOR of V st x in z * M holds
x in z * N

let x be VECTOR of V; :: thesis: ( x in z * M implies x in z * N )
assume x in z * M ; :: thesis: x in z * N
then ex w being VECTOR of V st
( x = z * w & w in M ) ;
hence x in z * N by A1; :: thesis: verum

end;

hence z * M c= z * N ; :: thesis: verum