theorem Th22: :: MATRPROB:22

for M being Matrix of REAL holds ColSum M = LineSum (M @)