let M be Matrix of COMPLEX ; :: thesis: ColSum M = LineSum (M @ )
A1: len (LineSum (M @ )) = len (M @ ) by Def10;
A2: len (ColSum M) = width M by Def11;
then A3: len (ColSum M) = len (LineSum (M @ )) by A1, MATRIX_1:def 7;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len (ColSum M) implies (ColSum M) . i = (LineSum (M @ )) . i )
assume A4: ( 1 <= i & i <= len (ColSum M) ) ; :: thesis: (ColSum M) . i = (LineSum (M @ )) . i
then ( 1 <= i & i <= len (LineSum (M @ )) ) by A1, A2, MATRIX_1:def 7;
then i in Seg (len (LineSum (M @ ))) by FINSEQ_1:3;
then A5: i in Seg (len (M @ )) by Def10;
A6: i in Seg (width M) by A2, A4, FINSEQ_1:3;
hence (ColSum M) . i = Sum (Col M,i) by Def11
.= Sum (Line (M @ ),i) by A6, MATRIX_2:17
.= (LineSum (M @ )) . i by A5, Def10 ;
:: thesis: verum

end;

hence ColSum M = LineSum (M @ ) by A3, FINSEQ_1:18; :: thesis: verum