:: deftheorem defBilinearM defines BilinearM ZMODLAT1:def 32 :
for V1, V2 being free finite-rank Z_Module
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for f being bilinear-FrForm of V1,V2
for b₆ being Matrix of len b1, len b2,F_Real holds
( b₆ = BilinearM (f,b1,b2) iff for i, j being Nat st i in dom b1 & j in dom b2 holds
b₆ * (i,j) = f . ((b1 /. i),(b2 /. j)) );