let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for V, W being non empty ModuleStr over K
for f being Functional of V
for v being Vector of V
for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0. K
let V, W be non empty ModuleStr over K; :: thesis: for f being Functional of V
for v being Vector of V
for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0. K
let f be Functional of V; :: thesis: for v being Vector of V
for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0. K
let v be Vector of V; :: thesis: for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0. K
let y be Vector of W; :: thesis: (FormFunctional (f,(0Functional W))) . (v,y) = 0. K
set 0F = 0Functional W;
set F = FormFunctional (f,(0Functional W));
thus (FormFunctional (f,(0Functional W))) . (v,y) = (f . v) * ((0Functional W) . y) by Def10
.= (f . v) * (0. K) by FUNCOP_1:7
.= 0. K ; :: thesis: verum