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 :: thesis: for v being Element of R holds (1 (*) LR) . v = LR . v
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 8 ; :: thesis: verum
end;
hence 1 (*) LR = LR ; :: thesis: verum