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 A1: 0. X in r * M ; :: thesis: 0. X in M
consider v being Point of X such that
A2: r * v = 0. X and
A3: v in M by A1;
r * (0. X) = 0. X by RLVECT_1:23;
hence 0. X in M by A2, A3, RLVECT_1:50; :: thesis: verum