:: deftheorem Def3 defines * ZMODLAT1:def 12 :
for V, W being non empty ModuleStr over INT.Ring
for f being FrForm of V,W
for a being Element of F_Real
for b₅ being FrForm of V,W holds
( b₅ = a * f iff for v being Vector of V
for w being Vector of W holds b₅ . (v,w) = a * (f . (v,w)) );