let X be RealLinearSpace; :: thesis: for M being Subset of X
for r being non zero Real st 0. X in r * M holds
0. X in M
let M be Subset of X; :: thesis: for r being non zero Real st 0. X in r * M holds
0. X in M
let r be non zero Real; :: thesis: ( 0. X in r * M implies 0. X in M )
assume 0. X in r * M ; :: thesis: 0. X in M
then A1: ex v being Point of X st
( r * v = 0. X & v in M ) ;
r * (0. X) = 0. X ;
hence 0. X in M by A1, RLVECT_1:36; :: thesis: verum