let V1, V2 be free finite-rank Z_Module; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for b3 being OrdBasis of V1
for f being bilinear-Form of V1,V2 st 0 < rank V1 holds
BilinearM (f,b3,b2) = (AutMt ((id V1),b3,b1)) * (BilinearM (f,b1,b2))
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for b3 being OrdBasis of V1
for f being bilinear-Form of V1,V2 st 0 < rank V1 holds
BilinearM (f,b3,b2) = (AutMt ((id V1),b3,b1)) * (BilinearM (f,b1,b2))
let b2 be OrdBasis of V2; :: thesis: for b3 being OrdBasis of V1
for f being bilinear-Form of V1,V2 st 0 < rank V1 holds
BilinearM (f,b3,b2) = (AutMt ((id V1),b3,b1)) * (BilinearM (f,b1,b2))
let b3 be OrdBasis of V1; :: thesis: for f being bilinear-Form of V1,V2 st 0 < rank V1 holds
BilinearM (f,b3,b2) = (AutMt ((id V1),b3,b1)) * (BilinearM (f,b1,b2))
let f be bilinear-Form of V1,V2; :: thesis: ( 0 < rank V1 implies BilinearM (f,b3,b2) = (AutMt ((id V1),b3,b1)) * (BilinearM (f,b1,b2)) )
assume AS: 0 < rank V1 ; :: thesis: BilinearM (f,b3,b2) = (AutMt ((id V1),b3,b1)) * (BilinearM (f,b1,b2))
set n = len b3;
A1: len b1 = rank V1 by ThRank1;
A3: len b3 = rank V1 by ThRank1;
reconsider IM1 = AutMt ((id V1),b3,b1) as Matrix of len b3,INT.Ring by LMThMBF3, A3;
reconsider M1 = IM1 as Matrix of len b3,INT.Ring ;
set M2 = M1 * (BilinearM (f,b1,b2));
B1: ( len M1 = len b3 & width M1 = len b3 & Indices M1 = [:(Seg (len b3)),(Seg (len b3)):] ) by MATRIX_0:24;
0 < len b1 by AS, ThRank1;
then B3: ( len (BilinearM (f,b1,b2)) = len b1 & width (BilinearM (f,b1,b2)) = len b2 ) by MATRIX_0:23;
then ( len (M1 * (BilinearM (f,b1,b2))) = len b3 & width (M1 * (BilinearM (f,b1,b2))) = len b2 ) by A1, A3, B1, MATRIX_3:def 4;
then reconsider M2 = M1 * (BilinearM (f,b1,b2)) as Matrix of len b3, len b2,INT.Ring by A3, AS, MATRIX_0:20;
set FM1 = M1;
set FBM = BilinearM (f,b1,b2);
for i, j being Nat st [i,j] in Indices (BilinearM (f,b3,b2)) holds
(BilinearM (f,b3,b2)) * (i,j) = M2 * (i,j)

proof

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

B13: now :: thesis: for k being Nat st k in Seg (len b1) holds
(Col ((BilinearM (f,b1,b2)),j)) . k = f . ((b1 /. k),(b2 /. j))

let k be Nat; :: thesis: ( k in Seg (len b1) implies (Col ((BilinearM (f,b1,b2)),j)) . k = f . ((b1 /. k),(b2 /. j)) )
assume B131: k in Seg (len b1) ; :: thesis: (Col ((BilinearM (f,b1,b2)),j)) . k = f . ((b1 /. k),(b2 /. j))
then B132: k in dom (BilinearM (f,b1,b2)) by B3, FINSEQ_1:def 3;
B81: k in dom b1 by FINSEQ_1:def 3, B131;
thus (Col ((BilinearM (f,b1,b2)),j)) . k = (BilinearM (f,b1,b2)) * (k,j) by B132, MATRIX_0:def 8
.= f . ((b1 /. k),(b2 /. j)) by B8, B81, defBilinearM ; :: thesis: verum

end;

B135: i in Seg (len b3) by B6, ZFMISC_1:87;
then B135A: i in dom M1 by B1, FINSEQ_1:def 3;
B136: i in dom b3 by B135, FINSEQ_1:def 3;

B15: now :: thesis: for k being Nat st 1 <= k & k <= len (Line (M1,i)) holds
(Line (M1,i)) . k = ((b3 /. i) |-- b1) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (Line (M1,i)) implies (Line (M1,i)) . k = ((b3 /. i) |-- b1) . k )
assume BX131: ( 1 <= k & k <= len (Line (M1,i)) ) ; :: thesis: (Line (M1,i)) . k = ((b3 /. i) |-- b1) . k
then B131: k in Seg (len b1) by FINSEQ_1:1, B12, A1, A3;
[i,k] in Indices M1 by A1, A3, B1, B131, B135, ZFMISC_1:87;
then consider p being FinSequence of INT.Ring such that
B133: ( p = M1 . i & M1 * (i,k) = p . k ) by MATRIX_0:def 5;
X0: (Line (M1,i)) . k = M1 * (i,k) by B1, B12, BX131, FINSEQ_1:1, MATRIX_0:def 7
.= (AutMt ((id V1),b3,b1)) * (i,k) ;
M1 . i = (AutMt ((id V1),b3,b1)) /. i by B135A, PARTFUN1:def 6
.= ((id V1) . (b3 /. i)) |-- b1 by B136, Def8 ;
hence (Line (M1,i)) . k = ((b3 /. i) |-- b1) . k by B133, X0; :: thesis: verum

end;

len (Line (M1,i)) = len ((b3 /. i) |-- b1) by A1, A3, B12, Def7;
hence (BilinearM (f,b3,b2)) * (i,j) = M2 * (i,j) by A1, A3, B9, B11, B12, B13, B14, B15, LMThMBF1Y, FINSEQ_1:def 18; :: thesis: verum

end;

hence BilinearM (f,b3,b2) = (AutMt ((id V1),b3,b1)) * (BilinearM (f,b1,b2)) by MATRIX_0:27; :: thesis: verum