let K be Field; :: thesis: for V2, V1 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1 st len b1 > 0 & f is linear holds
(LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2) = LineVec2Mx ((f . v1) |-- b2)
let V2, V1 be finite-dimensional VectSp of K; :: thesis: for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1 st len b1 > 0 & f is linear holds
(LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2) = LineVec2Mx ((f . v1) |-- b2)
let f be Function of V1,V2; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for v1 being Element of V1 st len b1 > 0 & f is linear holds
(LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2) = LineVec2Mx ((f . v1) |-- b2)
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for v1 being Element of V1 st len b1 > 0 & f is linear holds
(LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2) = LineVec2Mx ((f . v1) |-- b2)
let b2 be OrdBasis of V2; :: thesis: for v1 being Element of V1 st len b1 > 0 & f is linear holds
(LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2) = LineVec2Mx ((f . v1) |-- b2)
let v1 be Element of V1; :: thesis: ( len b1 > 0 & f is linear implies (LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2) = LineVec2Mx ((f . v1) |-- b2) )
assume A1: ( len b1 > 0 & f is linear ) ; :: thesis: (LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2) = LineVec2Mx ((f . v1) |-- b2)
set vb = v1 |-- b1;
set fb = (f . v1) |-- b2;
set L = LineVec2Mx (v1 |-- b1);
set A = AutMt f,b1,b2;
set LA = (LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2);
set Lf = LineVec2Mx ((f . v1) |-- b2);
A2: ( len (v1 |-- b1) = len b1 & len ((f . v1) |-- b2) = len b2 ) by MATRLIN:def 9;
then A3: ( len (LineVec2Mx (v1 |-- b1)) = 1 & width (LineVec2Mx (v1 |-- b1)) = len b1 ) by MATRIX_1:24;
A4: ( len (AutMt f,b1,b2) = len b1 & width (AutMt f,b1,b2) = len b2 ) by A1, MATRLIN:44, MATRLIN:def 10;
then A5: ( len ((LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2)) = 1 & width ((LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2)) = len b2 ) by A3, MATRIX_3:def 4;
A6: ( len (LineVec2Mx ((f . v1) |-- b2)) = 1 & width (LineVec2Mx ((f . v1) |-- b2)) = len b2 ) by A2, MATRIX_1:24;

now

let i, j be Nat; :: thesis: ( [i,j] in Indices ((LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2)) implies (LineVec2Mx ((f . v1) |-- b2)) * i,j = ((LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2)) * i,j )
assume A7: [i,j] in Indices ((LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2)) ; :: thesis: (LineVec2Mx ((f . v1) |-- b2)) * i,j = ((LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2)) * i,j
A8: ( i in dom ((LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2)) & dom ((LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2)) = Seg 1 & dom b2 = Seg (len b2) & j in Seg (len b2) ) by A5, A7, FINSEQ_1:def 3, ZFMISC_1:106;
then A9: i = 1 by FINSEQ_1:4, TARSKI:def 1;
A10: ( len (f * b1) = len b1 & len (Col (AutMt f,b1,b2),j) = len (AutMt f,b1,b2) ) by FINSEQ_1:def 18, FINSEQ_2:37;

A11: now

let k be Nat; :: thesis: ( k in dom (Col (AutMt f,b1,b2),j) implies (Col (AutMt f,b1,b2),j) . k = (((f * b1) /. k) |-- b2) . j )
assume A12: k in dom (Col (AutMt f,b1,b2),j) ; :: thesis: (Col (AutMt f,b1,b2),j) . k = (((f * b1) /. k) |-- b2) . j
A13: ( dom (AutMt f,b1,b2) = dom (Col (AutMt f,b1,b2),j) & dom (AutMt f,b1,b2) = Seg (len (AutMt f,b1,b2)) & dom (AutMt f,b1,b2) = dom b1 & dom (f * b1) = dom b1 ) by A4, A10, FINSEQ_1:def 3, FINSEQ_3:31;
then A14: (AutMt f,b1,b2) . k = (AutMt f,b1,b2) /. k by A12, PARTFUN1:def 8;
A15: f . (b1 /. k) = f . (b1 . k) by A12, A13, PARTFUN1:def 8
.= (f * b1) . k by A12, A13, FUNCT_1:23
.= (f * b1) /. k by A12, A13, PARTFUN1:def 8 ;
thus (Col (AutMt f,b1,b2),j) . k = (AutMt f,b1,b2) * k,j by A12, A13, MATRIX_1:def 9
.= (Line (AutMt f,b1,b2),k) . j by A8, A4, MATRIX_1:def 8
.= ((AutMt f,b1,b2) /. k) . j by A4, A12, A13, A14, MATRIX_2:10
.= (((f * b1) /. k) |-- b2) . j by A15, A12, A13, MATRLIN:def 10 ; :: thesis: verum

end;

thus (LineVec2Mx ((f . v1) |-- b2)) * i,j = (Line (LineVec2Mx ((f . v1) |-- b2)),i) . j by A6, A8, MATRIX_1:def 8
.= ((f . v1) |-- b2) . j by A9, MATRIX15:25
.= ((f . (Sum (lmlt (v1 |-- b1),b1))) |-- b2) . j by MATRLIN:40
.= ((Sum (lmlt (v1 |-- b1),(f * b1))) |-- b2) . j by A1, A2, MATRLIN:22
.= (v1 |-- b1) "*" (Col (AutMt f,b1,b2),j) by A1, A2, A4, A11, Th30, A8, A10
.= (Line (LineVec2Mx (v1 |-- b1)),1) "*" (Col (AutMt f,b1,b2),j) by MATRIX15:25
.= ((LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2)) * i,j by A3, A4, A7, A9, MATRIX_3:def 4 ; :: thesis: verum

end;

hence (LineVec2Mx (v1 |-- b1)) * (AutMt f,b1,b2) = LineVec2Mx ((f . v1) |-- b2) by A5, A6, MATRIX_1:21; :: thesis: verum