let K be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; :: thesis: for V, W being non empty VectSpStr of K
for g being Functional of W
for v being Vector of V
for w being Vector of W holds (FormFunctional (0Functional V),g) . v,w = 0. K
let V, W be non empty VectSpStr of K; :: thesis: for g being Functional of W
for v being Vector of V
for w being Vector of W holds (FormFunctional (0Functional V),g) . v,w = 0. K
let h be Functional of W; :: thesis: for v being Vector of V
for w being Vector of W holds (FormFunctional (0Functional V),h) . v,w = 0. K
let v be Vector of V; :: thesis: for w being Vector of W holds (FormFunctional (0Functional V),h) . v,w = 0. K
let y be Vector of W; :: thesis: (FormFunctional (0Functional V),h) . v,y = 0. K
set 0F = 0Functional V;
set F = FormFunctional (0Functional V),h;
thus (FormFunctional (0Functional V),h) . v,y = ((0Functional V) . v) * (h . y) by Def11
.= (0. K) * (h . y) by FUNCOP_1:13
.= 0. K by VECTSP_1:39 ; :: thesis: verum