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