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 holds FormFunctional (f,(0Functional W)) = NulForm (V,W)
let V, W be non empty ModuleStr over K; :: thesis: for f being Functional of V holds FormFunctional (f,(0Functional W)) = NulForm (V,W)
let f be Functional of V; :: thesis: FormFunctional (f,(0Functional W)) = NulForm (V,W)

now :: thesis: for v being Vector of V
for y being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,y) = (NulForm (V,W)) . (v,y)

let v be Vector of V; :: thesis: for y being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,y) = (NulForm (V,W)) . (v,y)
let y be Vector of W; :: thesis: (FormFunctional (f,(0Functional W))) . (v,y) = (NulForm (V,W)) . (v,y)
thus (FormFunctional (f,(0Functional W))) . (v,y) = 0. K by Th20
.= (NulForm (V,W)) . (v,y) by FUNCOP_1:70 ; :: thesis: verum

end;

hence FormFunctional (f,(0Functional W)) = NulForm (V,W) ; :: thesis: verum