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 {}

hence r * M = {} ; :: thesis: verum

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

then
r * M c= {}
;
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;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

hence r * M = {} ; :: thesis: verum