let M be m-nonnegative Matrix of REAL; :: thesis: 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; :: 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_0:60
.= Infor_FinSeq_of (Line (M,k)) by A2, A1, Def8 ; :: thesis: verum