let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
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 V1 be finite-dimensional VectSp of K; :: 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 Def6
.= len (Sum M2) by A1, Def6 ;
hence (Sum (Sum M1)) + (Sum (Sum M2)) = Sum ((Sum M1) + (Sum M2)) by Th30
.= Sum (Sum (M1 ^^ M2)) by Th29 ;
:: thesis: verum