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

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

let y be Vector of W; :: thesis: (FunctionalFAF ((NulForm (V,W)),v)) . y = (0Functional W) . y
thus (FunctionalFAF ((NulForm (V,W)),v)) . y = (NulForm (V,W)) . (v,y) by BLTh8
.= 0. INT.Ring by FUNCOP_1:70
.= (0Functional W) . y ; :: thesis: verum

end;

hence FunctionalFAF ((NulForm (V,W)),v) = 0Functional W by FUNCT_2:63; :: thesis: verum