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 Th47
.= SumAll (M @) by Th48 ;
hence SumAll M = SumAll (M @) ; :: thesis: verum