let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; for V, W being non empty ModuleStr over K
for f being Functional of V holds FormFunctional (f,(0Functional W)) = NulForm (V,W)
let V, W be non empty ModuleStr over K; for f being Functional of V holds FormFunctional (f,(0Functional W)) = NulForm (V,W)
let f be Functional of V; FormFunctional (f,(0Functional W)) = NulForm (V,W)
now for v being Vector of V
for y being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,y) = (NulForm (V,W)) . (v,y)let v be
Vector of
V;
for y being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,y) = (NulForm (V,W)) . (v,y)let y be
Vector of
W;
(FormFunctional (f,(0Functional W))) . (v,y) = (NulForm (V,W)) . (v,y)thus (FormFunctional (f,(0Functional W))) . (
v,
y) =
0. K
by Th20
.=
(NulForm (V,W)) . (
v,
y)
by FUNCOP_1:70
;
verum end;
hence
FormFunctional (f,(0Functional W)) = NulForm (V,W)
; verum