let M be Matrix of REAL ; :: thesis: ( width M > 0 implies LineSum M = ColSum (M @ ) )
assume width M > 0 ; :: thesis: LineSum M = ColSum (M @ )
then A1: len M = width (M @ ) by MATRIX_2:12;
A2: len (LineSum M) = len M by Th20;
A3: len (ColSum (M @ )) = width (M @ ) by Def2;

A4: now

let i be Nat; :: thesis: ( 1 <= i & i <= len (ColSum (M @ )) implies (ColSum (M @ )) . i = (LineSum M) . i )
assume that
A5: 1 <= i and
A6: i <= len (ColSum (M @ )) ; :: thesis: (ColSum (M @ )) . i = (LineSum M) . i
i <= len (LineSum M) by A2, A1, A6, Def2;
then i in Seg (len (LineSum M)) by A5, FINSEQ_1:3;
then A7: i in Seg (len M) by Th20;
then A8: i in dom M by FINSEQ_1:def 3;
i in Seg (width (M @ )) by A3, A5, A6, FINSEQ_1:3;
hence (ColSum (M @ )) . i = Sum (Col (M @ ),i) by Def2
.= Sum (Line M,i) by A8, MATRIX_2:16
.= (LineSum M) . i by A7, Th20 ;
:: thesis: verum

end;

len (ColSum (M @ )) = len (LineSum M) by A2, A1, Def2;
hence LineSum M = ColSum (M @ ) by A4, FINSEQ_1:18; :: thesis: verum