let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))

let V1 be finite-dimensional VectSp of K; :: thesis: for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))
defpred S1[ Nat] means for M being Matrix of the carrier of V1 st len M = \$1 holds
Sum (Sum M) = Sum (Sum (M @));
let M be Matrix of the carrier of V1; :: thesis: Sum (Sum M) = Sum (Sum (M @))
A1: for P being FinSequence of V1 holds Sum () = Sum (Sum ())
proof
defpred S2[ FinSequence of V1] means Sum (Sum <*\$1*>) = Sum (Sum (<*\$1*> @));
let P be FinSequence of V1; :: thesis: Sum () = Sum (Sum ())
len <*(<*> the carrier of V1)*> = 1 by MATRIX_0:def 2;
then width <*(<*> the carrier of V1)*> = 0 by MATRIX_0:20;
then A2: len (<*(<*> the carrier of V1)*> @) = 0 by MATRIX_0:def 6;
A3: for P being FinSequence of V1
for x being Element of V1 st S2[P] holds
S2[P ^ <*x*>]
proof
let P be FinSequence of V1; :: thesis: for x being Element of V1 st S2[P] holds
S2[P ^ <*x*>]

let x be Element of V1; :: thesis: ( S2[P] implies S2[P ^ <*x*>] )
assume A4: Sum () = Sum (Sum ()) ; :: thesis: S2[P ^ <*x*>]
Seg (len ()) = dom () by FINSEQ_1:def 3
.= () /\ () by PRE_POLY:def 4
.= (Seg 1) /\ () by FINSEQ_1:38
.= (Seg 1) /\ (Seg 1) by FINSEQ_1:38
.= Seg 1 ;
then A5: len () = 1 by FINSEQ_1:6
.= len <*(P ^ <*x*>)*> by FINSEQ_1:39 ;
then A6: dom () = Seg (len <*(P ^ <*x*>)*>) by FINSEQ_1:def 3;
A7: now :: thesis: for i being Nat st i in dom () holds
() . i = <*(P ^ <*x*>)*> . i
let i be Nat; :: thesis: ( i in dom () implies () . i = <*(P ^ <*x*>)*> . i )
assume A8: i in dom () ; :: thesis: () . i = <*(P ^ <*x*>)*> . i
then i in {1} by ;
then A9: i = 1 by TARSKI:def 1;
reconsider m1 = <*P*> . i, m2 = . i as FinSequence ;
thus () . i = m1 ^ m2 by
.= P ^ m2 by
.= P ^ <*x*> by
.= <*(P ^ <*x*>)*> . i by ; :: thesis: verum
end;
per cases ( len P = 0 or len P <> 0 ) ;
suppose len P = 0 ; :: thesis: S2[P ^ <*x*>]
then A10: P = {} ;
hence Sum (Sum <*(P ^ <*x*>)*>) = Sum () by FINSEQ_1:34
.= Sum (Sum ()) by Th15
.= Sum (Sum (<*(P ^ <*x*>)*> @)) by ;
:: thesis: verum
end;
suppose A11: len P <> 0 ; :: thesis: S2[P ^ <*x*>]
A12: len = 1 by FINSEQ_1:40;
then A13: width = len <*x*> by MATRIX_0:20
.= 1 by FINSEQ_1:40 ;
then A14: len () = 1 by MATRIX_0:def 6;
A15: len <*P*> = 1 by FINSEQ_1:40;
then A16: width <*P*> = len P by MATRIX_0:20;
then A17: len () = len P by MATRIX_0:def 6;
width () = 1 by ;
then reconsider d1 = <*P*> @ as Matrix of len P,1, the carrier of V1 by ;
A18: len <*(P ^ <*x*>)*> = 1 by FINSEQ_1:40;
then A19: width <*(P ^ <*x*>)*> = len (P ^ <*x*>) by MATRIX_0:20
.= (len P) + () by FINSEQ_1:22
.= (len P) + 1 by FINSEQ_1:40 ;
A20: (<*<*x*>*> @) @ = by ;
A21: width () = len <*P*> by
.= width () by ;
then width () = 1 by ;
then reconsider d2 = @ as Matrix of 1,1, the carrier of V1 by ;
A22: (d1 ^ d2) @ = (() @) ^^ (() @) by
.= <*P*> ^^ by
.= <*(P ^ <*x*>)*> by
.= (<*(P ^ <*x*>)*> @) @ by ;
A23: len (() ^ ()) = (len ()) + (len ()) by FINSEQ_1:22
.= () + (len ()) by MATRIX_0:def 6
.= () + () by MATRIX_0:def 6
.= len (<*(P ^ <*x*>)*> @) by ;
thus Sum (Sum <*(P ^ <*x*>)*>) = Sum (Sum ()) by
.= (Sum (Sum ())) + (Sum ()) by A4, A15, A12, Th31
.= (Sum (Sum ())) + (Sum (Sum ())) by Th15
.= Sum ((Sum d1) ^ (Sum d2)) by RLVECT_1:41
.= Sum (Sum (d1 ^ d2)) by Th27
.= Sum (Sum (<*(P ^ <*x*>)*> @)) by ; :: thesis: verum
end;
end;
end;
<*(<*> the carrier of V1)*> is Matrix of 0 + 1, 0 , the carrier of V1 ;
then Sum (Sum <*(<*> the carrier of V1)*>) = 0. V1 by Th14
.= Sum (Sum (<*(<*> the carrier of V1)*> @)) by ;
then A24: S2[ <*> the carrier of V1] ;
for P being FinSequence of V1 holds S2[P] from hence Sum () = Sum (Sum ()) ; :: thesis: verum
end;
A25: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A26: for M being Matrix of the carrier of V1 st len M = n holds
Sum (Sum M) = Sum (Sum (M @)) ; :: thesis: S1[n + 1]
thus for M being Matrix of the carrier of V1 st len M = n + 1 holds
Sum (Sum M) = Sum (Sum (M @)) :: thesis: verum
proof
let M be Matrix of the carrier of V1; :: thesis: ( len M = n + 1 implies Sum (Sum M) = Sum (Sum (M @)) )
assume A27: len M = n + 1 ; :: thesis: Sum (Sum M) = Sum (Sum (M @))
A28: M <> {} by A27;
A29: dom M = Seg (len M) by FINSEQ_1:def 3;
per cases ( n = 0 or n > 0 ) ;
suppose A30: n = 0 ; :: thesis: Sum (Sum M) = Sum (Sum (M @))
then M . 1 = Line (M,1) by ;
then reconsider G = M . 1 as FinSequence of V1 ;
M = <*G*> by ;
hence Sum (Sum M) = Sum (Sum (M @)) by A1; :: thesis: verum
end;
suppose A31: n > 0 ; :: thesis: Sum (Sum M) = Sum (Sum (M @))
A32: M . (n + 1) = Line (M,(n + 1)) by ;
then reconsider M1 = M . (n + 1) as FinSequence of V1 ;
len M1 = width M by ;
then reconsider R = <*M1*> as Matrix of 1, width M, the carrier of V1 ;
reconsider M9 = M as Matrix of n + 1, width M, the carrier of V1 by ;
reconsider W = Del (M9,(n + 1)) as Matrix of n, width M, the carrier of V1 by Th3;
A33: width W = width M9 by
.= width R by Th2 ;
A34: len (W @) = width W by MATRIX_0:def 6
.= len (R @) by ;
A35: len (Del (M,(n + 1))) = n by ;
thus Sum (Sum M) = Sum (Sum (W ^ R)) by
.= Sum ((Sum W) ^ (Sum R)) by Th27
.= (Sum (Sum (Del (M,(n + 1))))) + (Sum (Sum R)) by RLVECT_1:41
.= (Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum R)) by
.= (Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum (R @))) by A1
.= Sum (Sum ((W @) ^^ (R @))) by
.= Sum (Sum ((W ^ R) @)) by
.= Sum (Sum (M @)) by ; :: thesis: verum
end;
end;
end;
end;
A36: S1[ 0 ]
proof
let M be Matrix of the carrier of V1; :: thesis: ( len M = 0 implies Sum (Sum M) = Sum (Sum (M @)) )
assume A37: len M = 0 ; :: thesis: Sum (Sum M) = Sum (Sum (M @))
then width M = 0 by MATRIX_0:def 3;
then A38: len (M @) = 0 by MATRIX_0:def 6;
thus Sum (Sum M) = 0. V1 by
.= Sum (Sum (M @)) by ; :: thesis: verum
end;
for n being Nat holds S1[n] from then S1[ len M] ;
hence Sum (Sum M) = Sum (Sum (M @)) ; :: thesis: verum