theorem ThMBF1: :: ZMODLAT1:96

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