let K be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; :: thesis: for V, W being non empty ModuleStr over 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 ModuleStr over 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 Def10

.= (0. K) * (h . y) by FUNCOP_1:7

.= 0. K ; :: thesis: verum

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 ModuleStr over 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 Def10

.= (0. K) * (h . y) by FUNCOP_1:7

.= 0. K ; :: thesis: verum