let V be non empty CLSStruct ; :: thesis: for M being empty Subset of V
for z being Complex holds z * M = {}
let M be empty Subset of V; :: thesis: for z being Complex holds z * M = {}
let z be Complex; :: thesis: z * M = {}
now :: thesis: for x being VECTOR of V st x in z * M holds
x in {}
let x be VECTOR of V; :: thesis: ( x in z * M implies x in {} )
assume x in z * M ; :: thesis: x in {}
then ex v being VECTOR of V st
( x = z * v & v in {} ) ;
hence x in {} ; :: thesis: verum
end;
then z * M c= {} ;
hence z * M = {} ; :: thesis: verum