let V, W be non empty ModuleStr over INT.Ring ; :: thesis: for g being FrFunctional of W
for v being Vector of V
for w being Vector of W holds (FrFormFunctional ((0FrFunctional V),g)) . (v,w) = 0. INT.Ring
let h be FrFunctional of W; :: thesis: for v being Vector of V
for w being Vector of W holds (FrFormFunctional ((0FrFunctional V),h)) . (v,w) = 0. INT.Ring
let v be Vector of V; :: thesis: for w being Vector of W holds (FrFormFunctional ((0FrFunctional V),h)) . (v,w) = 0. INT.Ring
let y be Vector of W; :: thesis: (FrFormFunctional ((0FrFunctional V),h)) . (v,y) = 0. INT.Ring
set 0F = 0FrFunctional V;
set F = FrFormFunctional ((0FrFunctional V),h);
thus (FrFormFunctional ((0FrFunctional V),h)) . (v,y) = ((0FrFunctional V) . v) * (h . y) by HDef10
.= (0. INT.Ring) * (h . y) by FUNCOP_1:7
.= 0. INT.Ring ; :: thesis: verum