let x be Vector of V; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds (0Functional V) . (a * x) = (a *' ) * ((0Functional V) . x)
let r be Scalar of ; :: thesis: (0Functional V) . (r * x) = (r *' ) * ((0Functional V) . x)
A1: (0Functional V) . x = 0. F_Complex by HAHNBAN1:22;
thus (0Functional V) . (r * x) = 0. F_Complex by HAHNBAN1:22
.= (r *' ) * ((0Functional V) . x) by A1, VECTSP_1:39 ; :: thesis: verum