let V be non empty CLSStruct ; :: thesis: for M being empty Subset of
for z being Complex holds z * M = {}
let M be empty Subset of ; :: thesis: for z being Complex holds z * M = {}
let z be Complex; :: thesis: z * M = {}

now

let x be VECTOR of ; :: thesis: ( x in z * M implies x in {} )
assume x in z * M ; :: thesis: x in {}
then ex v being VECTOR of st
( x = z * v & v in {} ) ;
hence x in {} ; :: thesis: verum

end;

then z * M c= {} by SUBSET_1:7;
hence z * M = {} ; :: thesis: verum