let V, W be non empty ModuleStr over INT.Ring ; :: thesis: for g being FrFunctional of W holds FrFormFunctional ((0FrFunctional V),g) = NulFrForm (V,W)
let h be FrFunctional of W; :: thesis: FrFormFunctional ((0FrFunctional V),h) = NulFrForm (V,W)

now :: thesis: for v being Vector of V
for y being Vector of W holds (FrFormFunctional ((0FrFunctional V),h)) . (v,y) = (NulFrForm (V,W)) . (v,y)

let v be Vector of V; :: thesis: for y being Vector of W holds (FrFormFunctional ((0FrFunctional V),h)) . (v,y) = (NulFrForm (V,W)) . (v,y)
let y be Vector of W; :: thesis: (FrFormFunctional ((0FrFunctional V),h)) . (v,y) = (NulFrForm (V,W)) . (v,y)
thus (FrFormFunctional ((0FrFunctional V),h)) . (v,y) = 0. INT.Ring by HTh21
.= (NulFrForm (V,W)) . (v,y) by FUNCOP_1:70 ; :: thesis: verum

end;

hence FrFormFunctional ((0FrFunctional V),h) = NulFrForm (V,W) ; :: thesis: verum