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