let M be m-nonnegative Matrix of REAL ; :: thesis: for k being Element of NAT st k in dom M holds
Line (Infor_FinSeq_of M),k = Infor_FinSeq_of (Line M,k)
let k be Element of NAT ; :: thesis: ( k in dom M implies Line (Infor_FinSeq_of M),k = Infor_FinSeq_of (Line M,k) )
assume A1: k in dom M ; :: thesis: 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 A2: dom (Infor_FinSeq_of M) = dom M by FINSEQ_3:31;
hence Line (Infor_FinSeq_of M),k = (Infor_FinSeq_of M) . k by A1, MATRIX_2:18
.= Infor_FinSeq_of (Line M,k) by A1, A2, Def8 ;
:: thesis: verum