let K be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; :: thesis: for V, W being non empty VectSpStr of K
for g being Functional of W holds FormFunctional (0Functional V),g = NulForm V,W
let V, W be non empty VectSpStr of K; :: thesis: for g being Functional of W holds FormFunctional (0Functional V),g = NulForm V,W
let h be Functional of W; :: thesis: FormFunctional (0Functional V),h = NulForm V,W

now

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

end;

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