theorem LMThMBF1X: :: ZMODLAT1:91

for V1, V2 being free finite-rank Z_Module
for b2, b3 being OrdBasis of V2
for f being bilinear-FrForm of V1,V2
for v1 being Vector of V1
for v2 being Vector of V2
for X, Y being FinSequence of F_Real st len X = len b2 & len Y = len b2 & ( for k being Nat st k in Seg (len b2) holds
Y . k = f . (v1,(b2 /. k)) ) & X = v2 |-- b2 holds
Y "*" X = f . (v1,v2)