let D be non empty set ; :: thesis: for M being Matrix of D holds Sum (Width <*M*>) = width M
let M be Matrix of D; :: thesis: Sum (Width <*M*>) = width M
Width <*M*> = <*(width M)*> by Th19;
hence Sum (Width <*M*>) = width M by RVSUM_1:73; :: thesis: verum