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

for v being Element of V st v in 1 * M holds

v in M

hence 1 * M = M by A2; :: thesis: verum

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

then A2:
M c= 1 * M
;
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;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

for v being Element of V st v in 1 * M holds

v in M

proof

then
1 * M c= M
;
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;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

hence 1 * M = M by A2; :: thesis: verum