let x be Vector of V; :: according to HAHNBAN1:def 18 :: thesis: for r being Real holds (0RFunctional V) . ([**r,0 **] * x) = r * ((0RFunctional V) . x)
let r be Real; :: thesis: (0RFunctional V) . ([**r,0 **] * x) = r * ((0RFunctional V) . x)
(0RFunctional V) . x = 0 by FUNCOP_1:13;
hence (0RFunctional V) . ([**r,0 **] * x) = r * ((0RFunctional V) . x) by FUNCOP_1:13; :: thesis: verum