let i be Nat; 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; ( i in Seg (len M) implies Line (M,i) = (Line ((M *'),i)) *' )
assume A1:
i in Seg (len M)
; 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;
( 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))
;
(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
;
verum
end;
hence
Line (M,i) = (Line ((M *'),i)) *'
by A2, A3, FINSEQ_1:14; verum