let D be non empty set ; for M being Matrix of D
for i being Nat st i in dom M holds
Line (M,i) = Col ((M @),i)
let M be Matrix of D; for i being Nat st i in dom M holds
Line (M,i) = Col ((M @),i)
let i be Nat; ( i in dom M implies Line (M,i) = Col ((M @),i) )
A1:
len (M @) = width M
by Def6;
len (Col ((M @),i)) = len (M @)
by Def8;
then A2:
len (Col ((M @),i)) = width M
by Def6;
then A3:
dom (Col ((M @),i)) = Seg (width M)
by FINSEQ_1:def 3;
assume A4:
i in dom M
; Line (M,i) = Col ((M @),i)
A5:
now for j being Nat st j in dom (Col ((M @),i)) holds
(Line (M,i)) . j = (Col ((M @),i)) . jlet j be
Nat;
( j in dom (Col ((M @),i)) implies (Line (M,i)) . j = (Col ((M @),i)) . j )A6:
dom (M @) = Seg (len (M @))
by FINSEQ_1:def 3;
assume A7:
j in dom (Col ((M @),i))
;
(Line (M,i)) . j = (Col ((M @),i)) . jthen
(
(Line (M,i)) . j = M * (
i,
j) &
[i,j] in Indices M )
by A4, A3, Def7, ZFMISC_1:87;
hence (Line (M,i)) . j =
(M @) * (
j,
i)
by Def6
.=
(Col ((M @),i)) . j
by A1, A3, A7, A6, Def8
;
verum end;
len (Line (M,i)) = width M
by Def7;
hence
Line (M,i) = Col ((M @),i)
by A2, A5, FINSEQ_2:9; verum