let K be non empty ZeroStr ; :: thesis: for V, W being non empty ModuleStr over K
for w being Vector of W holds FunctionalSAF ((NulForm (V,W)),w) = 0Functional V
let V, W be non empty ModuleStr over K; :: 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 Th9
.= 0. K by FUNCOP_1:70
.= (0Functional V) . v by HAHNBAN1:14 ; :: thesis: verum

end;

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