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

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

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 ; :: according to TARSKI:def 3 :: thesis: ( not x in AR or x in 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;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

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