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

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

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