for V1 being free finite-rank Z_Module
for b1 being OrdBasis of V1
for i, j being Nat st i in dom b1 & j in dom b1 holds
( ( i = j implies ((b1 /. i) |-- b1) . j = 1 ) & ( i <> j implies ((b1 /. i) |-- b1) . j = 0 ) )