let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ; :: thesis: for M being Subset of V holds 1r * M = M
let M be Subset of V; :: thesis: 1r * M = M
for v being Element of V st v in M holds
v in 1r * M

proof

let v be Element of V; :: thesis: ( v in M implies v in 1r * M )
A1: v = 1r * v by CLVECT_1:def 5;
assume v in M ; :: thesis: v in 1r * M
hence v in 1r * M by A1; :: thesis: verum

end;

then A2: M c= 1r * M ;
for v being Element of V st v in 1r * M holds
v in M

proof

let v be Element of V; :: thesis: ( v in 1r * M implies v in M )
assume v in 1r * M ; :: thesis: v in M
then ex x being Element of V st
( v = 1r * x & x in M ) ;
hence v in M by CLVECT_1:def 5; :: thesis: verum

end;

then 1r * M c= M ;
hence 1r * M = M by A2, XBOOLE_0:def 10; :: thesis: verum