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

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

hence
1 (*) LR = LR
; :: thesis: verumlet 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;thus (1 (*) LR) . v = LR . ((1 ") * v) by Def2

.= LR . v by RLVECT_1:def 8 ; :: thesis: verum