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_0:def 7;
A3: len ((Line ((M *'),i)) *') = len (Line ((M *'),i)) by COMPLSP2:def 1
.= width (M *') by MATRIX_0:def 7
.= 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:1;
A5: 1 <= i by A1, FINSEQ_1:1;
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:1;
then A9: j in Seg (width (M *')) by Def1;
j <= len ((Line ((M *'),i)) *') by A3, A7, MATRIX_0:def 7;
then A10: j <= len (Line ((M *'),i)) by COMPLSP2:def 1;
j <= width M by A7, MATRIX_0:def 7;
then A11: [i,j] in Indices M by A6, A5, A4, Th1;
(Line (M,i)) . j = ((M * (i,j)) *') *' by A8, MATRIX_0:def 7
.= ((M *') * (i,j)) *' by A11, Def1
.= ((Line ((M *'),i)) . j) *' by A9, MATRIX_0:def 7
.= ((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:14; :: thesis: verum