theorem Th11: :: RLAFFIN1:11

for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R holds 1 * AR = AR