let M be Matrix of REAL; :: thesis: ColSum M = LineSum (M @)
A1: len (ColSum M) = width M by Def2;
A2: len (LineSum (M @)) = len (M @) by Th20;

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;
then A6: i in Seg (len (M @)) by Th20;
A7: i in Seg (width M) by A1, A4, A5;
hence (ColSum M) . i = Sum (Col (M,i)) by Def2
.= Sum (Line ((M @),i)) by A7, MATRIX_0:59
.= (LineSum (M @)) . i by A6, Th20 ;
:: thesis: verum

end;

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