let M be Matrix of COMPLEX; ColSum M = LineSum (M @)
A1:
len (ColSum M) = width M
by Def10;
A2:
len (LineSum (M @)) = len (M @)
by Def9;
A3:
now for i being Nat st 1 <= i & i <= len (ColSum M) holds
(ColSum M) . i = (LineSum (M @)) . ilet i be
Nat;
( 1 <= i & i <= len (ColSum M) implies (ColSum M) . i = (LineSum (M @)) . i )assume that A4:
1
<= i
and A5:
i <= len (ColSum M)
;
(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, FINSEQ_1:1;
then A6:
i in Seg (len (M @))
by Def9;
A7:
i in Seg (width M)
by A1, A4, A5, FINSEQ_1:1;
hence (ColSum M) . i =
Sum (Col (M,i))
by Def10
.=
Sum (Line ((M @),i))
by A7, MATRIX_0:59
.=
(LineSum (M @)) . i
by A6, Def9
;
verum end;
len (ColSum M) = len (LineSum (M @))
by A2, A1, MATRIX_0:def 6;
hence
ColSum M = LineSum (M @)
by A3, FINSEQ_1:14; verum