let V be Z_Module; :: thesis: for L being Z_Linear_Combination of V holds 0 * L = Z_ZeroLC V
let L be Z_Linear_Combination of V; :: thesis: 0 * L = Z_ZeroLC V
let v be VECTOR of V; :: according to ZMODUL02:def 24 :: thesis: (0 * L) . v = (Z_ZeroLC V) . v
thus (0 * L) . v = 0 * (L . v) by Def26
.= (Z_ZeroLC V) . v by Th9 ; :: thesis: verum