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

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

let v be Vector of V; :: thesis: (FrFunctionalSAF ((NulFrForm (V,W)),y)) . v = (0FrFunctional V) . v
thus (FrFunctionalSAF ((NulFrForm (V,W)),y)) . v = (NulFrForm (V,W)) . (v,y) by HTh9
.= 0. INT.Ring by FUNCOP_1:70
.= (0FrFunctional V) . v by FUNCOP_1:7 ; :: thesis: verum

end;

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