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