let M be Matrix of ExtREAL; :: thesis:
assume A0: for i being Nat st i in dom M holds
not -infty in rng (M . i) ; :: thesis:
defpred S₁[ Nat] means for M being Matrix of ExtREAL st len M = $1 & ( for i being Nat st i in dom M holds
not -infty in rng (M . i) ) holds
SumAll M = SumAll (M @);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A2: for M being Matrix of ExtREAL st len M = n & ( for i being Nat st i in dom M holds
not -infty in rng (M . i) ) holds
SumAll M = SumAll (M @) ; :: thesis:
thus for M being Matrix of ExtREAL st len M = n + 1 & ( for i being Nat st i in dom M holds
not -infty in rng (M . i) ) holds
SumAll M = SumAll (M @) :: thesis:

proof

let M be Matrix of ExtREAL; :: thesis:
assume A3: ( len M = n + 1 & ( for i being Nat st i in dom M holds
not -infty in rng (M . i) ) ) ; :: thesis:
then a3: M <> {} ;

per cases ;

suppose A4: n = 0 ; :: thesis:

1 <= len M by A3, NAT_1:11;
then A5: not -infty in rng (M . 1) by A3, FINSEQ_3:25;
M = <*(M . 1)*> by A3, A4, FINSEQ_1:40;
hence SumAll M = SumAll (M @) by A5, Th26; :: thesis:

end;

suppose A30: n > 0 ; :: thesis:

reconsider M9 = M as Matrix of n + 1, width M,ExtREAL by A3, MATRIX_0:20;
reconsider M1 = M . (n + 1) as FinSequence of ExtREAL ;
reconsider w = Del (M9,(n + 1)) as Matrix of n, width M,ExtREAL by MATRLIN:3;
V1: 1 <= n + 1 by NAT_1:11;
then M . (n + 1) = Line (M,(n + 1)) by A3, FINSEQ_3:25, MATRIX_0:60;
then Y11: len M1 = width M by MATRIX_0:def 7;
then reconsider r = <*M1*> as Matrix of 1, width M,ExtREAL ;
A31: width w = width M9 by A30, MATRLIN:2
.= width r by MATRLIN:2 ;
A32: len (w @) = width w by MATRIX_0:def 6
.= len (r @) by A31, MATRIX_0:def 6 ;
A33: len (Del (M,(n + 1))) = n by A3, PRE_POLY:12;
T5: not -infty in rng M1 by V1, A3, FINSEQ_3:25;
for v being object st v in dom (Sum w) holds
(Sum w) . v <> -infty

proof

let v be object ; :: thesis:
assume P1: v in dom (Sum w) ; :: thesis:
then reconsider i = v as Nat ;
P2: (Sum w) . v = Sum (w . i) by P1, Def5;
( 1 <= i & i <= len (Sum w) ) by P1, FINSEQ_3:25;
then P3: ( 1 <= i & i <= len w ) by Def5;
then S0: ( 1 <= i & i <= n + 1 ) by A33, NAT_1:12;
R1: i in dom w by P3, FINSEQ_3:25;
then P4: w . i = Line (w,i) by MATRIX_0:60;
for j being Nat st j in dom (Line (w,i)) holds
(Line (w,i)) . j <> -infty

proof

let j be Nat; :: thesis:
assume j in dom (Line (w,i)) ; :: thesis:
then ( 1 <= j & j <= len (Line (w,i)) ) by FINSEQ_3:25;
then ( 1 <= j & j <= width w ) by MATRIX_0:def 7;
then P6: j in Seg (width w) ;
then [i,j] in [:(dom w),(Seg (width w)):] by R1, ZFMISC_1:def 2;
then [i,j] in Indices w by MATRIX_0:def 4;
then consider F being FinSequence of ExtREAL such that
R7: ( F = w . i & w * (i,j) = F . j ) by MATRIX_0:def 5;
M <> {} by A3;
then M = (Del (M,(len M))) ^ <*(M . (len M))*> by PRE_POLY:13;
then M . i = w . i by A3, R1, FINSEQ_1:def 7;
then S2: not -infty in rng F by R7, A3, S0, FINSEQ_3:25;
len F = width w by P4, R7, MATRIX_0:def 7;
then j in dom F by P6, FINSEQ_1:def 3;
then F . j in rng F by FUNCT_1:3;
hence (Line (w,i)) . j <> -infty by R7, S2, P6, MATRIX_0:def 7; :: thesis:

end;

hence (Sum w) . v <> -infty by P2, P4, Th17; :: thesis:

end;

then L1: not -infty in rng (Sum w) by FUNCT_1:def 3;
for v being object st v in dom (Sum r) holds
(Sum r) . v <> -infty

proof

let v be object ; :: thesis:
assume P1: v in dom (Sum r) ; :: thesis:
then reconsider i = v as Nat ;
P2: (Sum r) . v = Sum (r . i) by P1, Def5;
( 1 <= i & i <= len (Sum r) ) by P1, FINSEQ_3:25;
then P3: ( 1 <= i & i <= len r ) by Def5;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:40;
then i = 1 by XXREAL_0:1;
then n + i in Seg (n + 1) by FINSEQ_1:4;
then S0: n + i in dom M by A3, FINSEQ_1:def 3;
R1: i in dom r by P3, FINSEQ_3:25;
then P4: r . i = Line (r,i) by MATRIX_0:60;
for j being Nat st j in dom (Line (r,i)) holds
(Line (r,i)) . j <> -infty

proof

let j be Nat; :: thesis:
assume j in dom (Line (r,i)) ; :: thesis:
then ( 1 <= j & j <= len (Line (r,i)) ) by FINSEQ_3:25;
then ( 1 <= j & j <= width r ) by MATRIX_0:def 7;
then P6: j in Seg (width r) ;
then [i,j] in [:(dom r),(Seg (width r)):] by R1, ZFMISC_1:def 2;
then [i,j] in Indices r by MATRIX_0:def 4;
then consider F being FinSequence of ExtREAL such that
R7: ( F = r . i & r * (i,j) = F . j ) by MATRIX_0:def 5;
M <> {} by A3;
then M = w ^ <*(M . (n + 1))*> by A3, PRE_POLY:13;
then M . (n + i) = r . i by A33, R1, FINSEQ_1:def 7;
then S2: not -infty in rng F by R7, A3, S0;
len F = width r by P4, R7, MATRIX_0:def 7;
then j in dom F by P6, FINSEQ_1:def 3;
then F . j in rng F by FUNCT_1:3;
hence (Line (r,i)) . j <> -infty by R7, S2, P6, MATRIX_0:def 7; :: thesis:

end;

hence (Sum r) . v <> -infty by P2, P4, Th17; :: thesis:

end;

then T3: not -infty in rng (Sum r) by FUNCT_1:def 3;
T4: for i being Nat st i in dom (Del (M,(n + 1))) holds
not -infty in rng ((Del (M,(n + 1))) . i)

proof

let i be Nat; :: thesis:
assume R1: i in dom (Del (M,(n + 1))) ; :: thesis:
then P4: w . i = Line (w,i) by MATRIX_0:60;
( 1 <= i & i <= len w ) by R1, FINSEQ_3:25;
then S0: ( 1 <= i & i <= n + 1 ) by A33, NAT_1:12;
for v being object st v in dom (Line (w,i)) holds
(Line (w,i)) . v <> -infty

proof

let v be object ; :: thesis:
assume TT0: v in dom (Line (w,i)) ; :: thesis:
then reconsider j = v as Nat ;
( 1 <= j & j <= len (Line (w,i)) ) by TT0, FINSEQ_3:25;
then ( 1 <= j & j <= width w ) by MATRIX_0:def 7;
then P6: j in Seg (width w) ;
then [i,j] in [:(dom w),(Seg (width w)):] by R1, ZFMISC_1:def 2;
then [i,j] in Indices w by MATRIX_0:def 4;
then consider F being FinSequence of ExtREAL such that
R7: ( F = w . i & w * (i,j) = F . j ) by MATRIX_0:def 5;
M <> {} by A3;
then M = (Del (M,(len M))) ^ <*(M . (len M))*> by PRE_POLY:13;
then M . i = w . i by A3, R1, FINSEQ_1:def 7;
then S2: not -infty in rng F by R7, A3, S0, FINSEQ_3:25;
len F = width w by P4, R7, MATRIX_0:def 7;
then j in dom F by P6, FINSEQ_1:def 3;
then F . j in rng F by FUNCT_1:3;
hence (Line (w,i)) . v <> -infty by R7, S2, P6, MATRIX_0:def 7; :: thesis:

end;

hence not -infty in rng ((Del (M,(n + 1))) . i) by P4, FUNCT_1:def 3; :: thesis:

end;

M <> {} by A3;
then M = (Del (M,(len M))) ^ <*(M . (len M))*> by PRE_POLY:13;
then H1: M @ = (w @) ^^ (<*(M . (n + 1))*> @) by A3, A31, MATRLIN:28;
then Q4: dom (M @) = (dom (w @)) /\ (dom (<*(M . (n + 1))*> @)) by PRE_POLY:def 4;
dom (w @) = Seg (len (w @)) by FINSEQ_1:def 3;
then dom (w @) = Seg (width w) by MATRIX_0:def 6;
then dom (w @) = Seg (len (<*(M . (n + 1))*> @)) by A31, MATRIX_0:def 6;
then Z0: dom (w @) = dom (<*(M . (n + 1))*> @) by FINSEQ_1:def 3;
Y2: len <*(M . (n + 1))*> = 1 by FINSEQ_1:40;
then Z2: width <*(M . (n + 1))*> = width M by Y11, MATRIX_0:20;
T6: for i being Nat st i in dom (w @) holds
not -infty in rng ((w @) . i)

proof

let i be Nat; :: thesis:
assume R1: i in dom (w @) ; :: thesis:
then P4: (w @) . i = Line ((w @),i) by MATRIX_0:60;
( 1 <= i & i <= len (w @) ) by R1, FINSEQ_3:25;
then ( 1 <= i & i <= width w ) by MATRIX_0:def 6;
then 1 <= width w by XXREAL_0:2;
then V5: 1 <= width M by A30, MATRLIN:2;
for v being object st v in dom (Line ((w @),i)) holds
(Line ((w @),i)) . v <> -infty

proof

let v be object ; :: thesis:
assume TT0: v in dom (Line ((w @),i)) ; :: thesis:
then reconsider j = v as Nat ;
( 1 <= j & j <= len (Line ((w @),i)) ) by TT0, FINSEQ_3:25;
then ( 1 <= j & j <= width (w @) ) by MATRIX_0:def 7;
then P6: j in Seg (width (w @)) ;
then [i,j] in [:(dom (w @)),(Seg (width (w @))):] by R1, ZFMISC_1:def 2;
then [i,j] in Indices (w @) by MATRIX_0:def 4;
then consider F being FinSequence of ExtREAL such that
R7: ( F = (w @) . i & (w @) * (i,j) = F . j ) by MATRIX_0:def 5;
width (<*(M . (n + 1))*> @) = len <*(M . (n + 1))*> by V5, Z2, MATRIX_0:29;
then 1 in Seg (width (<*(M . (n + 1))*> @)) by Y2;
then [i,1] in [:(dom (<*(M . (n + 1))*> @)),(Seg (width (<*(M . (n + 1))*> @))):] by Z0, R1, ZFMISC_1:87;
then [i,1] in Indices (<*(M . (n + 1))*> @) by MATRIX_0:def 4;
then consider G being FinSequence of ExtREAL such that
Q7: ( G = (<*(M . (n + 1))*> @) . i & (<*(M . (n + 1))*> @) * (i,1) = G . 1 ) by MATRIX_0:def 5;
(M @) . i = F ^ G by R7, H1, Z0, Q4, R1, Q7, PRE_POLY:def 4;
then not -infty in rng (F ^ G) by Z0, Q4, R1, A3, Th27;
then not -infty in (rng F) \/ (rng G) by FINSEQ_1:31;
then S2: ( not -infty in rng F & not -infty in rng G ) by XBOOLE_0:def 3;
len F = width (w @) by P4, R7, MATRIX_0:def 7;
then j in dom F by P6, FINSEQ_1:def 3;
then F . j in rng F by FUNCT_1:3;
hence (Line ((w @),i)) . v <> -infty by R7, S2, P6, MATRIX_0:def 7; :: thesis:

end;

hence not -infty in rng ((w @) . i) by P4, FUNCT_1:def 3; :: thesis:

end;

T7: for i being Nat st i in dom (r @) holds
not -infty in rng ((r @) . i)

proof

let i be Nat; :: thesis:
assume R1: i in dom (r @) ; :: thesis:
then P4: (r @) . i = Line ((r @),i) by MATRIX_0:60;
( 1 <= i & i <= len (r @) ) by R1, FINSEQ_3:25;
then ( 1 <= i & i <= width r ) by MATRIX_0:def 6;
then 1 <= width r by XXREAL_0:2;
then M1: 1 <= width M9 by MATRLIN:2;
for v being object st v in dom (Line ((r @),i)) holds
(Line ((r @),i)) . v <> -infty

proof

let v be object ; :: thesis:
assume TT0: v in dom (Line ((r @),i)) ; :: thesis:
then reconsider j = v as Nat ;
( 1 <= j & j <= len (Line ((r @),i)) ) by TT0, FINSEQ_3:25;
then ( 1 <= j & j <= width (r @) ) by MATRIX_0:def 7;
then P6: j in Seg (width (r @)) ;
then [i,j] in [:(dom (r @)),(Seg (width (r @))):] by R1, ZFMISC_1:def 2;
then [i,j] in Indices (r @) by MATRIX_0:def 4;
then consider G being FinSequence of ExtREAL such that
R7: ( G = (r @) . i & (r @) * (i,j) = G . j ) by MATRIX_0:def 5;
1 <= width w by A30, M1, MATRLIN:2;
then width (w @) = len w by MATRIX_0:29;
then n in Seg (width (w @)) by A30, A33, FINSEQ_1:3;
then [i,n] in [:(dom (w @)),(Seg (width (w @))):] by Z0, R1, ZFMISC_1:87;
then [i,n] in Indices (w @) by MATRIX_0:def 4;
then consider F being FinSequence of ExtREAL such that
Q7: ( F = (w @) . i & (w @) * (i,n) = F . n ) by MATRIX_0:def 5;
(M @) . i = F ^ G by R7, H1, Z0, Q4, R1, Q7, PRE_POLY:def 4;
then not -infty in rng (F ^ G) by Z0, Q4, R1, A3, Th27;
then not -infty in (rng F) \/ (rng G) by FINSEQ_1:31;
then S2: ( not -infty in rng F & not -infty in rng G ) by XBOOLE_0:def 3;
len G = width (r @) by P4, R7, MATRIX_0:def 7;
then j in dom G by P6, FINSEQ_1:def 3;
then G . j in rng G by FUNCT_1:3;
hence (Line ((r @),i)) . v <> -infty by S2, R7, P6, MATRIX_0:def 7; :: thesis:

end;

hence not -infty in rng ((r @) . i) by P4, FUNCT_1:def 3; :: thesis:

end;

thus SumAll M = SumAll (w ^ r) by A3, PRE_POLY:13, a3
.= Sum ((Sum w) ^ (Sum r)) by Th23
.= (SumAll (Del (M,(n + 1)))) + (SumAll r) by T3, L1, EXTREAL1:10
.= (SumAll ((Del (M,(n + 1))) @)) + (SumAll r) by A2, A33, T4
.= (SumAll ((Del (M,(n + 1))) @)) + (SumAll (r @)) by T5, Th26
.= SumAll ((w @) ^^ (r @)) by A32, Th25, T6, T7
.= SumAll ((w ^ r) @) by A31, MATRLIN:28
.= SumAll (M @) by A3, PRE_POLY:13, a3 ; :: thesis:

end;

A34: S₁[ 0 ]

proof

let M be Matrix of ExtREAL; :: thesis:
assume A35: ( len M = 0 & ( for i being Nat st i in dom M holds
not -infty in rng (M . i) ) ) ; :: thesis:
then width M = 0 by MATRIX_0:def 3;
then A36: len (M @) = 0 by MATRIX_0:def 6;
thus SumAll M = 0 by A35, Th21
.= SumAll (M @) by A36, Th21 ; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A34, A1);
then S₁[ len M] ;
hence SumAll M = SumAll (M @) by A0; :: thesis: