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

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