defpred S₁[ Nat] means for N being Matrix of COMPLEX st $1 + 1 = len N holds
Sum (LineSum N) = Sum (ColSum N);
let M be Matrix of COMPLEX; :: thesis:
assume len M > 0 ; :: thesis:
then 0 + 1 <= len M by NAT_1:8;
then (0 + 1) - 1 <= (len M) - 1 by XREAL_1:9;
then A1: (len M) -' 1 = (len M) - 1 by XREAL_0:def 2;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
for N being Matrix of COMPLEX st (k + 1) + 1 = len N holds
Sum (LineSum N) = Sum (ColSum N)

proof

reconsider k1 = k + 1 as Element of NAT ;
let N be Matrix of COMPLEX; :: thesis:
consider n being Nat such that
A4: for x being object st x in rng N holds
ex p being FinSequence of COMPLEX st
( x = p & len p = n ) by MATRIX_0:9;
A5: rng (N | k1) c= rng N by FINSEQ_5:19;
then for x being object st x in rng (N | k1) holds
ex p being FinSequence of COMPLEX st
( x = p & len p = n ) by A4;
then reconsider N2 = N | k1 as Matrix of COMPLEX by MATRIX_0:9;
set g1 = LineSum N2;
consider n3 being Nat such that
A6: for x2 being object st x2 in rng N holds
ex s being FinSequence st
( s = x2 & len s = n3 ) by MATRIX_0:def 1;
set f3 = LineSum N;
A7: len (Line (N,((k + 1) + 1))) = width N by MATRIX_0:def 7;
assume A8: (k + 1) + 1 = len N ; :: thesis:
then A9: len N2 = k + 1 by FINSEQ_1:59, NAT_1:11;
A10: len (LineSum N2) = len N2 by Def9
.= k1 by A8, FINSEQ_1:59, NAT_1:11 ;
1 + k >= 1 by NAT_1:11;
then A11: len N2 >= 1 by A8, FINSEQ_1:59, NAT_1:11;
then A12: len N2 > 0 ;
1 in Seg (len N2) by A11, FINSEQ_1:1;
then 1 in dom N2 by FINSEQ_1:def 3;
then A13: N2 . 1 in rng N2 by FUNCT_1:3;
then ex s3 being FinSequence st
( s3 = N2 . 1 & len s3 = n3 ) by A5, A6;
then A14: width N2 = n3 by A13, A12, MATRIX_0:def 3;
A15: len N >= 1 by A8, NAT_1:11;
then A16: len N > 0 ;
1 in Seg (len N) by A15, FINSEQ_1:1;
then A17: 1 in dom N by FINSEQ_1:def 3;
then A18: N . 1 in rng N by FUNCT_1:3;
A19: ex s2 being FinSequence st
( s2 = N . 1 & len s2 = n3 ) by A6, A17, FUNCT_1:3;
then A20: width N2 = width N by A18, A14, A16, MATRIX_0:def 3;
len (LineSum N) = k1 + 1 by A8, Def9;
then A21: len ((LineSum N) | k1) = len (LineSum N2) by A10, FINSEQ_1:59, NAT_1:11;
A22: for n being Nat st 1 <= n & n <= len ((LineSum N) | k1) holds
((LineSum N) | k1) . n = (LineSum N2) . n

proof

let n be Nat; :: thesis:
assume that
A23: 1 <= n and
A24: n <= len ((LineSum N) | k1) ; :: thesis:
A25: n <= k1 + 1 by A10, A21, A24, NAT_1:13;
then A26: n in Seg (len N) by A8, A23, FINSEQ_1:1;
A27: for n1 being Nat st 1 <= n1 & n1 <= len (Line (N,n)) holds
(Line (N,n)) . n1 = (Line (N2,n)) . n1

proof

A28: N2 . n = N . n by A10, A21, A24, FINSEQ_3:112;
A29: n <= len N2 by A21, A24, Def9;
let n1 be Nat; :: thesis:
assume that
A30: 1 <= n1 and
A31: n1 <= len (Line (N,n)) ; :: thesis:
A32: n1 in Seg (len (Line (N,n))) by A30, A31, FINSEQ_1:1;
then A33: n1 in Seg (width N2) by A20, MATRIX_0:def 7;
A34: n1 in Seg (width N) by A32, MATRIX_0:def 7;
then n1 <= width N by FINSEQ_1:1;
then [n,n1] in Indices N by A8, A23, A25, A30, Th1;
then A35: ex pn being FinSequence of COMPLEX st
( pn = N . n & N * (n,n1) = pn . n1 ) by MATRIX_0:def 5;
n1 <= width N by A34, FINSEQ_1:1;
then n1 <= width N2 by A8, A18, A19, A14, MATRIX_0:def 3;
then A36: [n,n1] in Indices N2 by A23, A30, A29, Th1;
n1 in Seg (width N) by A32, MATRIX_0:def 7;
then (Line (N,n)) . n1 = N * (n,n1) by MATRIX_0:def 7
.= N2 * (n,n1) by A36, A35, A28, MATRIX_0:def 5
.= (Line (N2,n)) . n1 by A33, MATRIX_0:def 7 ;
hence (Line (N,n)) . n1 = (Line (N2,n)) . n1 ; :: thesis:

end;

len (Line (N,n)) = width N by MATRIX_0:def 7
.= width N2 by A8, A18, A19, A14, MATRIX_0:def 3
.= len (Line (N2,n)) by MATRIX_0:def 7 ;
then A37: Line (N,n) = Line (N2,n) by A27, FINSEQ_1:14;
n in Seg (len ((LineSum N) | k1)) by A23, A24, FINSEQ_1:1;
then n in dom ((LineSum N) | k1) by FINSEQ_1:def 3;
then A38: n in dom ((LineSum N) | (Seg k1)) by FINSEQ_1:def 16;
n in Seg k1 by A10, A21, A23, A24, FINSEQ_1:1;
then A39: n in Seg (len N2) by A8, FINSEQ_1:59, NAT_1:11;
((LineSum N) | k1) . n = ((LineSum N) | (Seg k1)) . n by FINSEQ_1:def 16
.= (LineSum N) . n by A38, FUNCT_1:47
.= Sum (Line (N2,n)) by A26, A37, Def9
.= (LineSum N2) . n by A39, Def9 ;
hence ((LineSum N) | k1) . n = (LineSum N2) . n ; :: thesis:

end;

len (ColSum N2) = width N2 by Def10;
then A40: len ((ColSum N2) + (Line (N,((k + 1) + 1)))) = width N by A20, A7, COMPLSP2:6
.= len (ColSum N) by Def10 ;
A41: len (ColSum N2) = width N2 by Def10
.= width N by A8, A18, A19, A14, MATRIX_0:def 3
.= len (Line (N,((k + 1) + 1))) by MATRIX_0:def 7 ;
A42: (k + 1) + 1 in Seg (len N) by A8, FINSEQ_1:3;
then (k + 1) + 1 in Seg (len (LineSum N)) by Def9;
then A43: (k + 1) + 1 in dom (LineSum N) by FINSEQ_1:def 3;
A44: len N >= k + 1 by A8, NAT_1:11;
A45: for j being Nat st 1 <= j & j <= width N holds
((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j

proof

let j be Nat; :: thesis:
assume that
A46: 1 <= j and
A47: j <= width N ; :: thesis:
set g = Col (N2,j);
set f = Col (N,j);
A48: k1 <= len (Col (N,j)) by A44, MATRIX_0:def 8;
A49: for n being Nat st 1 <= n & n <= len ((Col (N,j)) | k1) holds
((Col (N,j)) | k1) . n = (Col (N2,j)) . n

proof

let n be Nat; :: thesis:
assume that
A50: 1 <= n and
A51: n <= len ((Col (N,j)) | k1) ; :: thesis:
A52: n <= k1 by A48, A51, FINSEQ_1:59;
then A53: N2 . n = N . n by FINSEQ_3:112;
n <= k1 + 1 by A52, NAT_1:13;
then n in Seg (len N) by A8, A50, FINSEQ_1:1;
then A54: n in dom N by FINSEQ_1:def 3;
n <= len N by A8, A52, NAT_1:13;
then [n,j] in Indices N by A46, A47, A50, Th1;
then A55: ex pn being FinSequence of COMPLEX st
( pn = N . n & N * (n,j) = pn . j ) by MATRIX_0:def 5;
A56: j <= width N2 by A8, A18, A19, A14, A47, MATRIX_0:def 3;
n in Seg k1 by A50, A52, FINSEQ_1:1;
then A57: n in dom N2 by A9, FINSEQ_1:def 3;
n in Seg (len ((Col (N,j)) | k1)) by A50, A51, FINSEQ_1:1;
then n in dom ((Col (N,j)) | k1) by FINSEQ_1:def 3;
then A58: n in dom ((Col (N,j)) | (Seg k1)) by FINSEQ_1:def 16;
n <= len N2 by A9, A48, A51, FINSEQ_1:59;
then A59: [n,j] in Indices N2 by A46, A50, A56, Th1;
((Col (N,j)) | k1) . n = ((Col (N,j)) | (Seg k1)) . n by FINSEQ_1:def 16
.= (Col (N,j)) . n by A58, FUNCT_1:47
.= N * (n,j) by A54, MATRIX_0:def 8
.= N2 * (n,j) by A59, A55, A53, MATRIX_0:def 5
.= (Col (N2,j)) . n by A57, MATRIX_0:def 8 ;
hence ((Col (N,j)) | k1) . n = (Col (N2,j)) . n ; :: thesis:

end;

A60: (k + 1) + 1 in Seg (len N) by A8, FINSEQ_1:4;
then A61: (k + 1) + 1 in dom N by FINSEQ_1:def 3;
len (Col (N2,j)) = len N2 by MATRIX_0:def 8
.= k1 by A8, FINSEQ_1:59, NAT_1:11 ;
then A62: Col (N2,j) = (Col (N,j)) | k1 by A48, A49, FINSEQ_1:14, FINSEQ_1:59;
A63: len (Col (N,j)) = len N by MATRIX_0:def 8;
(k + 1) + 1 in Seg (len (Col (N,j))) by A60, MATRIX_0:def 8;
then A64: (k + 1) + 1 in dom (Col (N,j)) by FINSEQ_1:def 3;
A65: j in Seg (width N) by A46, A47, FINSEQ_1:1;
then ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (Sum (Col (N2,j))) + (N * (((k + 1) + 1),j)) by A20, Def10
.= (Sum (Col (N2,j))) + ((Col (N,j)) . ((k + 1) + 1)) by A61, MATRIX_0:def 8
.= (Sum (Col (N2,j))) + ((Col (N,j)) /. ((k + 1) + 1)) by A64, PARTFUN1:def 6
.= Sum (Col (N,j)) by A8, A63, A62, Th46
.= (ColSum N) . j by A65, Def10 ;
hence ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) = (ColSum N) . j ; :: thesis:

end;

A66: for j being Nat st 1 <= j & j <= len (ColSum N) holds
((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j

proof

let j be Nat; :: thesis:
assume that
A67: 1 <= j and
A68: j <= len (ColSum N) ; :: thesis:
j in Seg (len (ColSum N)) by A67, A68, FINSEQ_1:1;
then A69: j in Seg (width N2) by A20, Def10;
then A70: j <= width N by A20, FINSEQ_1:1;
j in Seg (len ((ColSum N2) + (Line (N,((k + 1) + 1))))) by A40, A67, A68, FINSEQ_1:1;
then j in dom ((ColSum N2) + (Line (N,((k + 1) + 1)))) by FINSEQ_1:def 3;
then ((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = ((ColSum N2) . j) + ((Line (N,((k + 1) + 1))) . j) by COMPLSP2:1
.= ((ColSum N2) . j) + (N * (((k + 1) + 1),j)) by A20, A69, MATRIX_0:def 7
.= (ColSum N) . j by A45, A67, A70 ;
hence ((ColSum N2) + (Line (N,((k + 1) + 1)))) . j = (ColSum N) . j ; :: thesis:

end;

len (LineSum N) = len N by Def9;
then Sum (LineSum N) = (Sum (LineSum N2)) + ((LineSum N) /. ((k + 1) + 1)) by A8, A21, A22, Th46, FINSEQ_1:14
.= (Sum (LineSum N2)) + ((LineSum N) . ((k + 1) + 1)) by A43, PARTFUN1:def 6
.= (Sum (ColSum N2)) + ((LineSum N) . ((k + 1) + 1)) by A3, A9
.= (Sum (ColSum N2)) + (Sum (Line (N,((k + 1) + 1)))) by A42, Def9
.= Sum ((ColSum N2) + (Line (N,((k + 1) + 1)))) by A41, Th34
.= Sum (ColSum N) by A40, A66, FINSEQ_1:14 ;
hence Sum (LineSum N) = Sum (ColSum N) ; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

for N being Matrix of COMPLEX st 0 + 1 = len N holds
Sum (LineSum N) = Sum (ColSum N)

proof

let N be Matrix of COMPLEX; :: thesis:
A71: len (Line (N,1)) = width N by MATRIX_0:def 7;
assume A72: 0 + 1 = len N ; :: thesis:
then A73: 1 in Seg (len N) by FINSEQ_1:3;
A74: 1 in Seg 1 by FINSEQ_1:3;
A75: for j being Nat st 1 <= j & j <= width N holds
(ColSum N) . j = (Line (N,1)) . j

proof

A76: 1 in dom N by A72, A74, FINSEQ_1:def 3;
let j be Nat; :: thesis:
assume that
A77: 1 <= j and
A78: j <= width N ; :: thesis:
A79: len (Col (N,j)) = 1 by A72, MATRIX_0:def 8;
A80: j in Seg (width N) by A77, A78, FINSEQ_1:1;
then (ColSum N) . j = Sum (Col (N,j)) by Def10
.= (Col (N,j)) . 1 by A79, Th45
.= N * (1,j) by A76, MATRIX_0:def 8
.= (Line (N,1)) . j by A80, MATRIX_0:def 7 ;
hence (ColSum N) . j = (Line (N,1)) . j ; :: thesis:

end;

A81: len (LineSum N) = 1 by A72, Def9;
len (ColSum N) = width N by Def10;
then Sum (ColSum N) = Sum (Line (N,1)) by A71, A75, FINSEQ_1:14
.= (LineSum N) . 1 by A73, Def9
.= Sum (LineSum N) by A81, Th45 ;
hence Sum (LineSum N) = Sum (ColSum N) ; :: thesis:

end;

then A82: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A82, A2);
then ( ((len M) -' 1) + 1 = len M implies Sum (LineSum M) = Sum (ColSum M) ) ;
hence Sum (LineSum M) = Sum (ColSum M) by A1; :: thesis: