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

now

let i be Nat; :: thesis: ( 1 <= i & i <= len (ColSum (M @ )) implies (ColSum (M @ )) . i = (LineSum M) . i )
assume A6: ( 1 <= i & i <= len (ColSum (M @ )) ) ; :: thesis: (ColSum (M @ )) . i = (LineSum M) . i
then ( 1 <= i & i <= len (LineSum M) ) by A2, A4, Def2;
then i in Seg (len (LineSum M)) by 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, 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;

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