let D be non empty set ; :: thesis: for M being Matrix of D
for i being Nat st i in dom M holds
dom (M . i) = Seg (width M)
let M be Matrix of D; :: thesis: for i being Nat st i in dom M holds
dom (M . i) = Seg (width M)
let i be Nat; :: thesis: ( i in dom M implies dom (M . i) = Seg (width M) )
assume i in dom M ; :: thesis: dom (M . i) = Seg (width M)
hence dom (M . i) = dom (Line (M,i)) by MATRIX_0:60
.= Seg (len (Line (M,i))) by FINSEQ_1:def 3
.= Seg (width M) by MATRIX_0:def 7 ;
:: thesis: verum