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