let V, W be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over INT.Ring ; :: thesis: for f being homogeneousSAF FrForm of V,W
for w being Vector of W holds f . ((0. V),w) = 0. F_Real
let f be homogeneousSAF FrForm of V,W; :: thesis: for w being Vector of W holds f . ((0. V),w) = 0. F_Real
let v be Vector of W; :: thesis: f . ((0. V),v) = 0. F_Real
thus f . ((0. V),v) = f . (((0. INT.Ring) * (0. V)),v) by VECTSP10:1
.= (0. INT.Ring) * (f . ((0. V),v)) by HTh31
.= 0. F_Real ; :: thesis: verum