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

A4: i <= len M by A1, FINSEQ_1:3;
A5: 1 <= i by A1, FINSEQ_1:3;
let j be Nat; :: thesis: ( 1 <= j & j <= len (Line M,i) implies (Line M,i) . j = ((Line (M *' ),i) *' ) . j )
assume that
A6: 1 <= j and
A7: j <= len (Line M,i) ; :: thesis: (Line M,i) . j = ((Line (M *' ),i) *' ) . j
A8: j in Seg (width M) by A2, A6, A7, FINSEQ_1:3;
then A9: j in Seg (width (M *' )) by Def1;
j <= len ((Line (M *' ),i) *' ) by A3, A7, MATRIX_1:def 8;
then A10: j <= len (Line (M *' ),i) by COMPLSP2:def 1;
j <= width M by A7, MATRIX_1:def 8;
then A11: [i,j] in Indices M by A6, A5, A4, Th1;
(Line M,i) . j = ((M * i,j) *' ) *' by A8, MATRIX_1:def 8
.= ((M *' ) * i,j) *' by A11, Def1
.= ((Line (M *' ),i) . j) *' by A9, MATRIX_1:def 8
.= ((Line (M *' ),i) *' ) . j by A6, A10, 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