let M be Matrix of ExtREAL; :: thesis: ( len (Sum M) = len M & ( for i being Nat st i in Seg (len M) holds
(Sum M) . i = Sum (Line (M,i)) ) )
thus len (Sum M) = len M by Def5; :: thesis: for i being Nat st i in Seg (len M) holds
(Sum M) . i = Sum (Line (M,i))
thus for k being Nat st k in Seg (len M) holds
(Sum M) . k = Sum (Line (M,k)) :: thesis: verum
proof
let k be Nat; :: thesis: ( k in Seg (len M) implies (Sum M) . k = Sum (Line (M,k)) )
assume A1: k in Seg (len M) ; :: thesis: (Sum M) . k = Sum (Line (M,k))
A2: k in dom M by A1, FINSEQ_1:def 3;
k in Seg (len (Sum M)) by A1, Def5;
then k in dom (Sum M) by FINSEQ_1:def 3;
hence (Sum M) . k = Sum (M . k) by Def5
.= Sum (Line (M,k)) by A2, MATRIX_0:60 ;
:: thesis: verum
end;