let v be VECTOR of V; :: according to ZMODUL02:def 24 :: thesis: (1 * L) . v = L . v
thus (1 * L) . v = 1 * (L . v) by Def26
.= L . v ; :: thesis: verum