let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds 0 * L = ZeroLC V

let L be Linear_Combination of V; :: thesis: 0 * L = ZeroLC V

let v be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis: (0 * L) . v = (ZeroLC V) . v

thus (0 * L) . v = 0 * (L . v) by Def11

.= (ZeroLC V) . v by Th20 ; :: thesis: verum

let L be Linear_Combination of V; :: thesis: 0 * L = ZeroLC V

let v be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis: (0 * L) . v = (ZeroLC V) . v

thus (0 * L) . v = 0 * (L . v) by Def11

.= (ZeroLC V) . v by Th20 ; :: thesis: verum