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);

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

hence
FunctionalSAF ((NulForm (V,W)),y) = 0Functional V
by FUNCT_2:63; :: thesis: verumlet 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;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