let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for LR being Linear_Combination of R holds 1 (*) LR = LR
let LR be Linear_Combination of R; :: thesis: 1 (*) LR = LR

now

let v be Element of R; :: thesis: (1 (*) LR) . v = LR . v
thus (1 (*) LR) . v = LR . ((1 ") * v) by Def2
.= LR . v by RLVECT_1:def 11 ; :: thesis: verum

end;

hence 1 (*) LR = LR by RLVECT_2:def 11; :: thesis: verum