let V1, V2 be free finite-rank Z_Module; :: thesis:
let b1 be OrdBasis of V1; :: thesis:
let b2, b3 be OrdBasis of V2; :: thesis:
let f be bilinear-FrForm of V1,V2; :: thesis:
set I = inttorealM (AutMt ((id V2),b3,b2));
assume AS: 0 < rank V1 ; :: thesis:
set n = len b2;
A2: len b2 = rank V2 by ZMATRLIN:49;
A3: len b3 = rank V2 by ZMATRLIN:49;
reconsider IM1 = AutMt ((id V2),b3,b2) as Matrix of len b2,INT.Ring by ZMATRLIN:50, A2;
reconsider M1 = inttorealM (IM1 @) as Matrix of len b2,F_Real ;
set M2 = (BilinearM (f,b1,b2)) * M1;
B1: ( len M1 = len b2 & width M1 = len b2 & Indices M1 = [:(Seg (len b2)),(Seg (len b2)):] ) by MATRIX_0:24;
F1: ( len IM1 = len b2 & width IM1 = len b2 & Indices IM1 = [:(Seg (len b2)),(Seg (len b2)):] ) by MATRIX_0:24;
B2: 0 < len b1 by AS, ZMATRLIN:49;
then B3: ( len (BilinearM (f,b1,b2)) = len b1 & width (BilinearM (f,b1,b2)) = len b2 ) by MATRIX_0:23;
C1: width (BilinearM (f,b1,b2)) = len M1 by B1, B2, MATRIX_0:23;
X0: ( len ((BilinearM (f,b1,b2)) * M1) = len b1 & width ((BilinearM (f,b1,b2)) * M1) = len b2 ) by B1, B3, MATRIX_3:def 4;
then reconsider M2 = (BilinearM (f,b1,b2)) * M1 as Matrix of len b1, len b2,F_Real by B2, MATRIX_0:20;
set FM1 = M1;
set FBM = BilinearM (f,b1,b2);
X1: ( len (BilinearM (f,b1,b3)) = len M2 & width (BilinearM (f,b1,b3)) = width M2 ) by A2, A3, B2, X0, MATRIX_0:23;
X2: M1 = (inttorealM (AutMt ((id V2),b3,b2))) @ by ZMATRLIN:6;
for i, j being Nat st [i,j] in Indices (BilinearM (f,b1,b3)) holds
(BilinearM (f,b1,b3)) * (i,j) = M2 * (i,j)

proof

let i, j be Nat; :: thesis:
assume [i,j] in Indices (BilinearM (f,b1,b3)) ; :: thesis:
then B6: [i,j] in [:(Seg (len b1)),(Seg (len b3)):] by B2, MATRIX_0:23;
then B7: ( i in Seg (len b1) & j in Seg (len b3) ) by ZFMISC_1:87;
then B8: ( i in dom b1 & j in dom b3 ) by FINSEQ_1:def 3;
then B9: (BilinearM (f,b1,b3)) * (i,j) = f . ((b1 /. i),(b3 /. j)) by defBilinearM;
[i,j] in Indices M2 by B2, B6, A2, A3, MATRIX_0:23;
then B11: M2 * (i,j) = (Line ((BilinearM (f,b1,b2)),i)) "*" (Col (M1,j)) by C1, MATRIX_3:def 4;
B12: len (Line ((BilinearM (f,b1,b2)),i)) = len b2 by B3, MATRIX_0:def 7;

B13: now :: thesis:

let k be Nat; :: thesis:
assume B131: k in Seg (len b2) ; :: thesis:
then B132: k in Seg (width (BilinearM (f,b1,b2))) by B2, MATRIX_0:23;
B81: k in dom b2 by FINSEQ_1:def 3, B131;
thus (Line ((BilinearM (f,b1,b2)),i)) . k = (BilinearM (f,b1,b2)) * (i,k) by B132, MATRIX_0:def 7
.= f . ((b1 /. i),(b2 /. k)) by B8, B81, defBilinearM ; :: thesis:

end;

B14: len (Col (M1,j)) = len b2 by B1, MATRIX_0:def 8;
B135: j in Seg (len b2) by B6, A2, A3, ZFMISC_1:87;

B15: now :: thesis:

let k be Nat; :: thesis:
assume ( 1 <= k & k <= len (Col (M1,j)) ) ; :: thesis:
then B131: k in Seg (len b2) by B14;
then B132: k in dom M1 by B1, FINSEQ_1:def 3;
B132A: j in dom IM1 by B135, F1, FINSEQ_1:def 3;
Y1: [j,k] in Indices IM1 by F1, B131, B135, ZFMISC_1:87;
then consider p being FinSequence of INT such that
B133: ( p = IM1 . j & IM1 * (j,k) = p . k ) by MATRIX_0:def 5;
B81A: j in dom b3 by B7, FINSEQ_1:def 3;
Y2: [k,j] in Indices (IM1 @) by Y1, MATRIX_0:def 6;
X0: (Col (M1,j)) . k = M1 * (k,j) by B132, MATRIX_0:def 8
.= (IM1 @) * (k,j) by Y2, ZMATRLIN:1
.= (AutMt ((id V2),b3,b2)) * (j,k) by Y1, MATRIX_0:def 6 ;
IM1 . j = (AutMt ((id V2),b3,b2)) /. j by B132A, PARTFUN1:def 6
.= ((id V2) . (b3 /. j)) |-- b2 by B81A, ZMATRLIN:def 8 ;
hence (Col (M1,j)) . k = ((b3 /. j) |-- b2) . k by B133, X0; :: thesis:

end;

len (Col (M1,j)) = len ((b3 /. j) |-- b2) by B14, ZMATRLIN:def 7;
hence (BilinearM (f,b1,b3)) * (i,j) = M2 * (i,j) by B9, B11, B12, B13, B14, B15, LMThMBF1X, FINSEQ_1:def 18; :: thesis:

end;

hence BilinearM (f,b1,b3) = (BilinearM (f,b1,b2)) * ((inttorealM (AutMt ((id V2),b3,b2))) @) by ZMATRLIN:4, X1, X2; :: thesis: