let M be Matrix of COMPLEX; :: thesis: ColSum M = LineSum (M @)
A1: len (ColSum M) = width M by Def10;
A2: len (LineSum (M @)) = len (M @) by Def9;

A3: now :: thesis: for i being Nat st 1 <= i & i <= len (ColSum M) holds
(ColSum M) . i = (LineSum (M @)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (ColSum M) implies (ColSum M) . i = (LineSum (M @)) . i )
assume that
A4: 1 <= i and
A5: i <= len (ColSum M) ; :: thesis: (ColSum M) . i = (LineSum (M @)) . i
i <= len (LineSum (M @)) by A2, A1, A5, MATRIX_0:def 6;
then i in Seg (len (LineSum (M @))) by A4, FINSEQ_1:1;
then A6: i in Seg (len (M @)) by Def9;
A7: i in Seg (width M) by A1, A4, A5, FINSEQ_1:1;
hence (ColSum M) . i = Sum (Col (M,i)) by Def10
.= Sum (Line ((M @),i)) by A7, MATRIX_0:59
.= (LineSum (M @)) . i by A6, Def9 ;
:: thesis: verum

end;

len (ColSum M) = len (LineSum (M @)) by A2, A1, MATRIX_0:def 6;
hence ColSum M = LineSum (M @) by A3, FINSEQ_1:14; :: thesis: verum