let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for V, W being non empty VectSpStr of K
for f being Functional of V holds FormFunctional f,(0Functional W) = NulForm V,W
let V, W be non empty VectSpStr of 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

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 Th21
.= (NulForm V,W) . v,y by FUNCOP_1:85 ; :: thesis: verum

end;

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