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

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

end;

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