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

A3: now

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_1:def 7;
then i in Seg (len (LineSum (M @ ))) by A4, FINSEQ_1:3;
then A6: i in Seg (len (M @ )) by Def10;
A7: i in Seg (width M) by A1, A4, A5, FINSEQ_1:3;
hence (ColSum M) . i = Sum (Col M,i) by Def11
.= Sum (Line (M @ ),i) by A7, MATRIX_2:17
.= (LineSum (M @ )) . i by A6, Def10 ;
:: thesis: verum

end;

len (ColSum M) = len (LineSum (M @ )) by A2, A1, MATRIX_1:def 7;
hence ColSum M = LineSum (M @ ) by A3, FINSEQ_1:18; :: thesis: verum