let x be Vector of V; :: according to HAHNBAN1:def 8 :: thesis: for r being Scalar of holds (0Functional V) . (r * x) = r * ((0Functional V) . x)
let r be Scalar of ; :: thesis: (0Functional V) . (r * x) = r * ((0Functional V) . x)
A1: (0Functional V) . x = 0. K by FUNCOP_1:7;
thus (0Functional V) . (r * x) = 0. K by FUNCOP_1:7
.= r * ((0Functional V) . x) by A1 ; :: thesis: verum