let K be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; :: thesis: for V, W being non empty ModuleStr over K

for g being Functional of W holds FormFunctional ((0Functional V),g) = NulForm (V,W)

let V, W be non empty ModuleStr over K; :: thesis: for g being Functional of W holds FormFunctional ((0Functional V),g) = NulForm (V,W)

let h be Functional of W; :: thesis: FormFunctional ((0Functional V),h) = NulForm (V,W)

for g being Functional of W holds FormFunctional ((0Functional V),g) = NulForm (V,W)

let V, W be non empty ModuleStr over K; :: thesis: for g being Functional of W holds FormFunctional ((0Functional V),g) = NulForm (V,W)

let h be Functional of W; :: thesis: FormFunctional ((0Functional V),h) = NulForm (V,W)

now :: thesis: for v being Vector of V

for y being Vector of W holds (FormFunctional ((0Functional V),h)) . (v,y) = (NulForm (V,W)) . (v,y)

hence
FormFunctional ((0Functional V),h) = NulForm (V,W)
; :: thesis: verumfor y being Vector of W holds (FormFunctional ((0Functional V),h)) . (v,y) = (NulForm (V,W)) . (v,y)

let v be Vector of V; :: thesis: for y being Vector of W holds (FormFunctional ((0Functional V),h)) . (v,y) = (NulForm (V,W)) . (v,y)

let y be Vector of W; :: thesis: (FormFunctional ((0Functional V),h)) . (v,y) = (NulForm (V,W)) . (v,y)

thus (FormFunctional ((0Functional V),h)) . (v,y) = 0. K by Th21

.= (NulForm (V,W)) . (v,y) by FUNCOP_1:70 ; :: thesis: verum

end;let y be Vector of W; :: thesis: (FormFunctional ((0Functional V),h)) . (v,y) = (NulForm (V,W)) . (v,y)

thus (FormFunctional ((0Functional V),h)) . (v,y) = 0. K by Th21

.= (NulForm (V,W)) . (v,y) by FUNCOP_1:70 ; :: thesis: verum