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)
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:31;
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 A2: k in dom M ; :: thesis: 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_2:18
.= Infor_FinSeq_of (Line M,k) by A2, A1, Def8 ; :: thesis: verum