let V, W be non empty ModuleStr over INT.Ring ; :: 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
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
let v be Vector of V; :: thesis: for w being Vector of W holds (FormFunctional ((0Functional V),h)) . (v,w) = 0
let y be Vector of W; :: thesis: (FormFunctional ((0Functional V),h)) . (v,y) = 0
set 0F = 0Functional V;
set F = FormFunctional ((0Functional V),h);
thus (FormFunctional ((0Functional V),h)) . (v,y) = ((0Functional V) . v) * (h . y) by BLDef10
.= 0 * (h . y)
.= 0 ; :: thesis: verum