for V1, V2 being free finite-rank Z_Module
for b1 being OrdBasis of V1
for f being bilinear-Form of V1,V2
for v1 being Vector of V1
for v2 being Vector of V2
for X, Y being FinSequence of INT.Ring 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)