let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for AR being Subset of R holds 1 * AR = AR
let AR be Subset of R; :: thesis: 1 * AR = AR
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: AR c= 1 * AR
let x be object ; :: thesis: ( x in 1 * AR implies x in AR )
assume x in 1 * AR ; :: thesis: x in AR
then ex v being Element of R st
( x = 1 * v & v in AR ) ;
hence x in AR by RLVECT_1:def 8; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in AR or x in 1 * AR )
assume A1: x in AR ; :: thesis: x in 1 * AR
reconsider v = x as Element of R by A1;
x = 1 * v by RLVECT_1:def 8;
hence x in 1 * AR by A1; :: thesis: verum