let M be m-nonnegative Matrix of REAL; for k being Nat st k in dom M holds
Line ((Infor_FinSeq_of M),k) = Infor_FinSeq_of (Line (M,k))
set M1 = Infor_FinSeq_of M;
len (Infor_FinSeq_of M) = len M
by Def8;
then A1:
dom (Infor_FinSeq_of M) = dom M
by FINSEQ_3:29;
let k be Nat; ( k in dom M implies Line ((Infor_FinSeq_of M),k) = Infor_FinSeq_of (Line (M,k)) )
assume A2:
k in dom M
; Line ((Infor_FinSeq_of M),k) = Infor_FinSeq_of (Line (M,k))
thus Line ((Infor_FinSeq_of M),k) =
(Infor_FinSeq_of M) . k
by A2, A1, MATRIX_0:60
.=
Infor_FinSeq_of (Line (M,k))
by A2, A1, Def8
; verum