let V, W be non empty ModuleStr over INT.Ring ; :: thesis: for v being Vector of V holds FrFunctionalFAF ((NulFrForm (V,W)),v) = 0FrFunctional W
let v be Vector of V; :: thesis: FrFunctionalFAF ((NulFrForm (V,W)),v) = 0FrFunctional W
set N = NulFrForm (V,W);

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

let y be Vector of W; :: thesis: (FrFunctionalFAF ((NulFrForm (V,W)),v)) . y = (0FrFunctional W) . y
thus (FrFunctionalFAF ((NulFrForm (V,W)),v)) . y = (NulFrForm (V,W)) . (v,y) by HTh8
.= 0. F_Real by FUNCOP_1:70
.= (0FrFunctional W) . y by FUNCOP_1:7 ; :: thesis: verum

end;

hence FrFunctionalFAF ((NulFrForm (V,W)),v) = 0FrFunctional W by FUNCT_2:63; :: thesis: verum