let K be non empty ZeroStr ; 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; for w being Vector of W holds FunctionalSAF ((NulForm (V,W)),w) = 0Functional V
let y be Vector of W; FunctionalSAF ((NulForm (V,W)),y) = 0Functional V
set N = NulForm (V,W);
hence
FunctionalSAF ((NulForm (V,W)),y) = 0Functional V
by FUNCT_2:63; verum