let M be Matrix of COMPLEX ; :: thesis: ( len M > 0 implies SumAll M = SumAll (M @ ) )
assume len M > 0 ; :: thesis: SumAll M = SumAll (M @ )
then SumAll M = Sum (ColSum M) by Th52
.= SumAll (M @ ) by Th53 ;
hence SumAll M = SumAll (M @ ) ; :: thesis: verum