let K be non empty ZeroStr ; :: thesis: for V, W being non empty VectSpStr of K
for v being Vector of V holds FunctionalFAF (NulForm V,W),v = 0Functional W
let V, W be non empty VectSpStr of K; :: 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

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 Th9
.= 0. K by FUNCOP_1:85
.= (0Functional W) . y by HAHNBAN1:22 ; :: thesis: verum

end;

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