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