let v be VECTOR of V; :: according to ZMODUL02:def 24 :: thesis: (L + (Z_ZeroLC V)) . v = L . v
reconsider N0 = 0 as Element of INT by INT_1:def 2;
thus (L + (Z_ZeroLC V)) . v = (L . v) + ((Z_ZeroLC V) . v) by Def25
.= (L . v) + N0 by Th9
.= L . v ; :: thesis: verum