let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for M being Subset of V holds 1 * M = M
let M be Subset of V; :: thesis: 1 * M = M
for v being Element of V st v in M holds
v in 1 * M
proof
let v be Element of V; :: thesis: ( v in M implies v in 1 * M )
A1: v = 1 * v by RLVECT_1:def 8;
assume v in M ; :: thesis: v in 1 * M
hence v in 1 * M by A1; :: thesis: verum
end;
then A2: M c= 1 * M ;
for v being Element of V st v in 1 * M holds
v in M
proof
let v be Element of V; :: thesis: ( v in 1 * M implies v in M )
assume v in 1 * M ; :: thesis: v in M
then ex x being Element of V st
( v = 1 * x & x in M ) ;
hence v in M by RLVECT_1:def 8; :: thesis: verum
end;
then 1 * M c= M ;
hence 1 * M = M by A2; :: thesis: verum