let M be Matrix of REAL; :: thesis: SumAll M = Sum (ColSum M)
thus Sum (ColSum M) = SumAll (M @) by Th22
.= SumAll M by Th28 ; :: thesis: verum