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

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

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

end;

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