theorem ThMBF2: :: ZMODLAT1:97

for V1, V2 being free finite-rank Z_Module
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V1
for f being bilinear-FrForm of V1,V2 st 0 < rank V1 holds
BilinearM (f,b3,b2) = (inttorealM (AutMt ((id V1),b3,b1))) * (BilinearM (f,b1,b2))