theorem ThMBF3: :: ZMODLAT1:98

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