let D be non empty set ; :: thesis: for M1, M2 being Matrix of D holds Sum (Width <*M1,M2*>) = (width M1) + (width M2)
let M1, M2 be Matrix of D; :: thesis: Sum (Width <*M1,M2*>) = (width M1) + (width M2)
thus Sum (Width <*M1,M2*>) = Sum ((Width <*M1*>) ^ (Width <*M2*>)) by Th18
.= (Sum (Width <*M1*>)) + (Sum (Width <*M2*>)) by RVSUM_1:75
.= (width M1) + (Sum (Width <*M2*>)) by Lm5
.= (width M1) + (width M2) by Lm5 ; :: thesis: verum