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

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