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