let M be Matrix of ExtREAL; ( ( for i being Nat st i in dom M holds
not -infty in rng (M . i) ) implies SumAll M = SumAll (M @) )
assume A0:
for i being Nat st i in dom M holds
not -infty in rng (M . i)
; SumAll M = SumAll (M @)
defpred S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
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 @)
;
S1[n + 1]
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 @)
verumproof
let M be
Matrix of
ExtREAL;
( len M = n + 1 & ( for i being Nat st i in dom M holds
not -infty in rng (M . i) ) implies SumAll M = SumAll (M @) )
assume A3:
(
len M = n + 1 & ( for
i being
Nat st
i in dom M holds
not
-infty in rng (M . i) ) )
;
SumAll M = SumAll (M @)
then a3:
M <> {}
;
per cases
( n = 0 or n > 0 )
;
suppose A30:
n > 0
;
SumAll M = SumAll (M @)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 ;
( v in dom (Sum w) implies (Sum w) . v <> -infty )
assume P1:
v in dom (Sum w)
;
(Sum w) . v <> -infty
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;
( j in dom (Line (w,i)) implies (Line (w,i)) . j <> -infty )
assume
j in dom (Line (w,i))
;
(Line (w,i)) . j <> -infty
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;
verum
end;
hence
(Sum w) . v <> -infty
by P2, P4, Th17;
verum
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 ;
( v in dom (Sum r) implies (Sum r) . v <> -infty )
assume P1:
v in dom (Sum r)
;
(Sum r) . v <> -infty
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;
( j in dom (Line (r,i)) implies (Line (r,i)) . j <> -infty )
assume
j in dom (Line (r,i))
;
(Line (r,i)) . j <> -infty
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;
verum
end;
hence
(Sum r) . v <> -infty
by P2, P4, Th17;
verum
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;
( i in dom (Del (M,(n + 1))) implies not -infty in rng ((Del (M,(n + 1))) . i) )
assume R1:
i in dom (Del (M,(n + 1)))
;
not -infty in rng ((Del (M,(n + 1))) . i)
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 ;
( v in dom (Line (w,i)) implies (Line (w,i)) . v <> -infty )
assume TT0:
v in dom (Line (w,i))
;
(Line (w,i)) . v <> -infty
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;
verum
end;
hence
not
-infty in rng ((Del (M,(n + 1))) . i)
by P4, FUNCT_1:def 3;
verum
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;
( i in dom (w @) implies not -infty in rng ((w @) . i) )
assume R1:
i in dom (w @)
;
not -infty in rng ((w @) . i)
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 ;
( v in dom (Line ((w @),i)) implies (Line ((w @),i)) . v <> -infty )
assume TT0:
v in dom (Line ((w @),i))
;
(Line ((w @),i)) . v <> -infty
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;
verum
end;
hence
not
-infty in rng ((w @) . i)
by P4, FUNCT_1:def 3;
verum
end; T7:
for
i being
Nat st
i in dom (r @) holds
not
-infty in rng ((r @) . i)
proof
let i be
Nat;
( i in dom (r @) implies not -infty in rng ((r @) . i) )
assume R1:
i in dom (r @)
;
not -infty in rng ((r @) . i)
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 ;
( v in dom (Line ((r @),i)) implies (Line ((r @),i)) . v <> -infty )
assume TT0:
v in dom (Line ((r @),i))
;
(Line ((r @),i)) . v <> -infty
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;
verum
end;
hence
not
-infty in rng ((r @) . i)
by P4, FUNCT_1:def 3;
verum
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
;
verum end;
end;
end;
A34:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A34, A1);
then
S1[ len M]
;
hence
SumAll M = SumAll (M @)
by A0; verum