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