let V1 be free finite-rank Z_Module; :: thesis: for M being Matrix of the carrier of V1 holds Sum (Sum M) = Sum (Sum (M @))
defpred S₁[ 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 <*P*>) = Sum (Sum (<*P*> @))

proof

defpred S₂[ FinSequence of V1] means Sum (Sum <*$1*>) = Sum (Sum (<*$1*> @));
let P be FinSequence of V1; :: thesis: Sum (Sum <*P*>) = Sum (Sum (<*P*> @))
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 S₂[P] holds
S₂[P ^ <*x*>]

proof

let P be FinSequence of V1; :: thesis: for x being Element of V1 st S₂[P] holds
S₂[P ^ <*x*>]
let x be Element of V1; :: thesis: ( S₂[P] implies S₂[P ^ <*x*>] )
assume A4: Sum (Sum <*P*>) = Sum (Sum (<*P*> @)) ; :: thesis: S₂[P ^ <*x*>]
Seg (len (<*P*> ^^ <*<*x*>*>)) = dom (<*P*> ^^ <*<*x*>*>) by FINSEQ_1:def 3
.= (dom <*P*>) /\ (dom <*<*x*>*>) by PRE_POLY:def 4
.= (Seg 1) /\ (dom <*<*x*>*>) by FINSEQ_1:38
.= (Seg 1) /\ (Seg 1) by FINSEQ_1:38
.= Seg 1 ;
then A5: len (<*P*> ^^ <*<*x*>*>) = 1 by FINSEQ_1:6
.= len <*(P ^ <*x*>)*> by FINSEQ_1:39 ;
then A6: dom (<*P*> ^^ <*<*x*>*>) = Seg (len <*(P ^ <*x*>)*>) by FINSEQ_1:def 3;

A7: now :: thesis: for i being Nat st i in dom (<*P*> ^^ <*<*x*>*>) holds
(<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i

let i be Nat; :: thesis: ( i in dom (<*P*> ^^ <*<*x*>*>) implies (<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i )
assume A8: i in dom (<*P*> ^^ <*<*x*>*>) ; :: thesis: (<*P*> ^^ <*<*x*>*>) . i = <*(P ^ <*x*>)*> . i
then i in {1} by A6, FINSEQ_1:2, FINSEQ_1:40;
then A9: i = 1 by TARSKI:def 1;
reconsider m1 = <*P*> . i, m2 = <*<*x*>*> . i as FinSequence ;
thus (<*P*> ^^ <*<*x*>*>) . i = m1 ^ m2 by A8, PRE_POLY:def 4
.= P ^ m2 by A9
.= P ^ <*x*> by A9
.= <*(P ^ <*x*>)*> . i by A9 ; :: thesis: verum

end;

per cases ( len P = 0 or len P <> 0 ) ;

suppose len P = 0 ; :: thesis: S₂[P ^ <*x*>]

then A10: P = {} ;
hence Sum (Sum <*(P ^ <*x*>)*>) = Sum (Sum <*<*x*>*>) by FINSEQ_1:34
.= Sum (Sum (<*<*x*>*> @)) by MATRLIN:15
.= Sum (Sum (<*(P ^ <*x*>)*> @)) by A10, FINSEQ_1:34 ;
:: thesis: verum

end;

suppose A11: len P <> 0 ; :: thesis: S₂[P ^ <*x*>]

A12: len <*<*x*>*> = 1 by FINSEQ_1:40;
then A13: width <*<*x*>*> = len <*x*> by MATRIX_0:20
.= 1 by FINSEQ_1:40 ;
then A14: len (<*<*x*>*> @) = 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 (<*P*> @) = len P by MATRIX_0:def 6;
width (<*P*> @) = 1 by A11, A15, A16, MATRIX_0:54;
then reconsider d1 = <*P*> @ as Matrix of len P,1, the carrier of V1 by A11, A17, MATRIX_0:20;
A18: len <*(P ^ <*x*>)*> = 1 by FINSEQ_1:40;
then A19: width <*(P ^ <*x*>)*> = len (P ^ <*x*>) by MATRIX_0:20
.= (len P) + (len <*x*>) by FINSEQ_1:22
.= (len P) + 1 by FINSEQ_1:40 ;
A20: (<*<*x*>*> @) @ = <*<*x*>*> by A12, A13, MATRIX_0:57;
A21: width (<*P*> @) = len <*P*> by A11, A16, MATRIX_0:54
.= width (<*<*x*>*> @) by A15, A12, A13, MATRIX_0:54 ;
then width (<*<*x*>*> @) = 1 by A11, A15, A16, MATRIX_0:54;
then reconsider d2 = <*<*x*>*> @ as Matrix of 1,1, the carrier of V1 by A14, MATRIX_0:20;
A22: (d1 ^ d2) @ = ((<*P*> @) @) ^^ ((<*<*x*>*> @) @) by A21, MATRLIN:28
.= <*P*> ^^ <*<*x*>*> by A11, A15, A16, A20, MATRIX_0:57
.= <*(P ^ <*x*>)*> by A5, A7, FINSEQ_2:9
.= (<*(P ^ <*x*>)*> @) @ by A18, A19, MATRIX_0:57 ;
A23: len ((<*P*> @) ^ (<*<*x*>*> @)) = (len (<*P*> @)) + (len (<*<*x*>*> @)) by FINSEQ_1:22
.= (width <*P*>) + (len (<*<*x*>*> @)) by MATRIX_0:def 6
.= (width <*P*>) + (width <*<*x*>*>) by MATRIX_0:def 6
.= len (<*(P ^ <*x*>)*> @) by A16, A13, A19, MATRIX_0:def 6 ;
thus Sum (Sum <*(P ^ <*x*>)*>) = Sum (Sum (<*P*> ^^ <*<*x*>*>)) by A5, A7, FINSEQ_2:9
.= (Sum (Sum (<*P*> @))) + (Sum (Sum <*<*x*>*>)) by A4, A15, A12, Th31
.= (Sum (Sum (<*P*> @))) + (Sum (Sum (<*<*x*>*> @))) by MATRLIN:15
.= Sum ((Sum d1) ^ (Sum d2)) by RLVECT_1:41
.= Sum (Sum (d1 ^ d2)) by Th27
.= Sum (Sum (<*(P ^ <*x*>)*> @)) by A23, A22, MATRIX_0:53 ; :: 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 A2, Th13 ;
then A24: S₂[ <*> the carrier of V1] ;
for P being FinSequence of V1 holds S₂[P] from FINSEQ_2:sch 2(A24, A3);
hence Sum (Sum <*P*>) = Sum (Sum (<*P*> @)) ; :: thesis: verum

end;

A25: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[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: S₁[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 A27, A29, FINSEQ_1:4, MATRIX_0:60;
then reconsider G = M . 1 as FinSequence of V1 ;
M = <*G*> by A27, A30, FINSEQ_1:40;
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 A27, A29, FINSEQ_1:4, MATRIX_0:60;
then reconsider M1 = M . (n + 1) as FinSequence of V1 ;
len M1 = width M by A32, MATRIX_0:def 7;
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 A27, MATRIX_0:20;
reconsider W = Del (M9,(n + 1)) as Matrix of n, width M, the carrier of V1 by MATRLIN:3;
A33: width W = width M9 by A31, MATRLIN:2
.= width R by MATRLIN:2 ;
A34: len (W @) = width W by MATRIX_0:def 6
.= len (R @) by A33, MATRIX_0:def 6 ;
A35: len (Del (M,(n + 1))) = n by A27, PRE_POLY:12;
thus Sum (Sum M) = Sum (Sum (W ^ R)) by A28, PRE_POLY:13, A27
.= 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 A26, A35
.= (Sum (Sum ((Del (M,(n + 1))) @))) + (Sum (Sum (R @))) by A1
.= Sum (Sum ((W @) ^^ (R @))) by A34, Th31
.= Sum (Sum ((W ^ R) @)) by A33, MATRLIN:28
.= Sum (Sum (M @)) by A28, PRE_POLY:13, A27 ; :: thesis: verum

end;

end;

end;

end;

A36: S₁[ 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 A37, Th13
.= Sum (Sum (M @)) by A38, Th13 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A36, A25);
then S₁[ len M] ;
hence Sum (Sum M) = Sum (Sum (M @)) ; :: thesis: verum