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_0:54;
A2: len (LineSum M) = len M by Th20;
A3: len (ColSum (M @)) = width (M @) by Def2;
A4: 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
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;
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;
hence (ColSum (M @)) . i = Sum (Col ((M @),i)) by Def2
.= Sum (Line (M,i)) by A8, MATRIX_0:58
.= (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; :: thesis: verum