let i be Nat; :: thesis: for M being Matrix of COMPLEX st i in Seg (len M) holds
Line M,i = (Line (M *' ),i) *'
let M be Matrix of COMPLEX ; :: thesis: ( i in Seg (len M) implies Line M,i = (Line (M *' ),i) *' )
assume A1: i in Seg (len M) ; :: thesis: Line M,i = (Line (M *' ),i) *'
A2: len (Line M,i) = width M by MATRIX_1:def 8;
A3: len ((Line (M *' ),i) *' ) = len (Line (M *' ),i) by COMPLSP2:def 1
.= width (M *' ) by MATRIX_1:def 8
.= width M by Def1 ;
for j being Nat st 1 <= j & j <= len (Line M,i) holds
(Line M,i) . j = ((Line (M *' ),i) *' ) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M,i) implies (Line M,i) . j = ((Line (M *' ),i) *' ) . j )
assume A4: ( 1 <= j & j <= len (Line M,i) ) ; :: thesis: (Line M,i) . j = ((Line (M *' ),i) *' ) . j
then A5: ( 1 <= j & j <= width M ) by MATRIX_1:def 8;
( 1 <= j & j <= len ((Line (M *' ),i) *' ) ) by A3, A4, MATRIX_1:def 8;
then A6: ( 1 <= j & j <= len (Line (M *' ),i) ) by COMPLSP2:def 1;
( 1 <= i & i <= len M ) by A1, FINSEQ_1:3;
then A7: [i,j] in Indices M by A5, Th1;
A8: j in Seg (width M) by A2, A4, FINSEQ_1:3;
then A9: j in Seg (width (M *' )) by Def1;
(Line M,i) . j = ((M * i,j) *' ) *' by A8, MATRIX_1:def 8
.= ((M *' ) * i,j) *' by A7, Def1
.= ((Line (M *' ),i) . j) *' by A9, MATRIX_1:def 8
.= ((Line (M *' ),i) *' ) . j by A6, COMPLSP2:def 1 ;
hence (Line M,i) . j = ((Line (M *' ),i) *' ) . j ; :: thesis: verum

end;

hence Line M,i = (Line (M *' ),i) *' by A2, A3, FINSEQ_1:18; :: thesis: verum