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

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

end;

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