let V be non empty RLSStruct ; :: thesis: for M being empty Subset of
for r being Real holds r * M = {}
let M be empty Subset of ; :: thesis: for r being Real holds r * M = {}
let r be Real; :: thesis: r * M = {}
for x being VECTOR of st x in r * M holds
x in {}

proof

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

end;

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