let m be Matrix of REAL; :: 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 Def1; :: 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, Def1;
then k in dom (Sum m) by FINSEQ_1:def 3;
hence (Sum m) . k = Sum (m . k) by Def1
.= Sum (Line (m,k)) by A2, MATRIX_0:60 ;
:: thesis: verum

end;