theorem LMThMBF1Y: :: ZMODLAT1:92

for V1, V2 being free finite-rank Z_Module
for b1 being OrdBasis of V1
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 b1 & len Y = len b1 & ( for k being Nat st k in Seg (len b1) holds
Y . k = f . ((b1 /. k),v2) ) & X = v1 |-- b1 holds
X "*" Y = f . (v1,v2)