let V1 be free finite-rank Z_Module; :: thesis: for M1, M2 being Matrix of the carrier of V1 st len M1 = len M2 holds
(Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2))
let M1, M2 be Matrix of the carrier of V1; :: thesis: ( len M1 = len M2 implies (Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2)) )
assume A1: len M1 = len M2 ; :: thesis: (Sum (Sum M1)) + (Sum (Sum M2)) = Sum (Sum (M1 ^^ M2))
len (Sum M1) = len M1 by MATRLIN:def 6
.= len (Sum M2) by A1, MATRLIN:def 6 ;
hence (Sum (Sum M1)) + (Sum (Sum M2)) = Sum ((Sum M1) + (Sum M2)) by Th30
.= Sum (Sum (M1 ^^ M2)) by Th29 ;
:: thesis: verum