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