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