let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds 1 * L = L
let L be Linear_Combination of V; :: thesis: 1 * L = L
let v be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis: (1 * L) . v = L . v
thus (1 * L) . v = 1 * (L . v) by Def11
.= L . v ; :: thesis: verum