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