:: deftheorem HDef10 defines FrFormFunctional ZMODLAT1:def 26 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrFunctional of V
for g being FrFunctional of W
for b₅ being FrForm of V,W holds
( b₅ = FrFormFunctional (f,g) iff for v being Vector of V
for w being Vector of W holds b₅ . (v,w) = (f . v) * (g . w) );