let M be Matrix of REAL; for p being FinSequence of REAL * st len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) holds
SumAll M = Sum (p . (len M))
let p be FinSequence of REAL * ; ( len p = len M & p . 1 = M . 1 & ( for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1)) ) implies SumAll M = Sum (p . (len M)) )
assume that
A1:
len p = len M
and
A2:
p . 1 = M . 1
and
A3:
for k being Nat st k >= 1 & k < len M holds
p . (k + 1) = (p . k) ^ (M . (k + 1))
; SumAll M = Sum (p . (len M))
per cases
( len M = 0 or len M > 0 )
;
suppose A5:
len M > 0
;
SumAll M = Sum (p . (len M))then A6:
len M >= 1
by NAT_1:14;
set q =
LineSum M;
A7:
len (LineSum M) = len M
by MATRPROB:def 1;
then consider qq being
FinSequence of
REAL such that A8:
len qq = len (LineSum M)
and A9:
qq . 1
= (LineSum M) . 1
and A10:
for
k being
Nat st
0 <> k &
k < len (LineSum M) holds
qq . (k + 1) = (qq . k) + ((LineSum M) . (k + 1))
and A11:
Sum (LineSum M) = qq . (len (LineSum M))
by A5, Th9, NAT_1:14;
A12:
len qq =
len M
by A8, MATRPROB:def 1
.=
len (Sum p)
by A1, MATRPROB:def 1
;
A13:
dom qq = Seg (len qq)
by FINSEQ_1:def 3;
A14:
len (Sum p) = len p
by MATRPROB:def 1;
then A15:
dom (Sum p) = dom p
by FINSEQ_3:29;
for
j being
Nat st
j in dom qq holds
qq . j = (Sum p) . j
proof
defpred S1[
Nat]
means ( $1
in dom qq implies
qq . $1
= (Sum p) . $1 );
A16:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A17:
S1[
k]
;
S1[k + 1]
assume A18:
k + 1
in dom qq
;
qq . (k + 1) = (Sum p) . (k + 1)
then A19:
k + 1
<= len qq
by A13, FINSEQ_1:1;
A20:
k + 1
in dom (Sum p)
by A1, A7, A14, A8, A13, A18, FINSEQ_1:def 3;
A21:
k + 1
in dom M
by A7, A8, A13, A18, FINSEQ_1:def 3;
k + 1
>= 1
by A13, A18, FINSEQ_1:1;
then A22:
(
k + 1
= 1 or
k + 1
> 1 )
by XXREAL_0:1;
per cases
( k + 1 = 1 or k >= 1 )
by A22, NAT_1:13;
suppose A23:
k + 1
= 1
;
qq . (k + 1) = (Sum p) . (k + 1)A24:
1
in Seg (len M)
by A6, FINSEQ_1:1;
then A25:
1
in dom M
by FINSEQ_1:def 3;
A26:
1
in dom p
by A1, A24, FINSEQ_1:def 3;
qq . (k + 1) =
Sum (Line (M,1))
by A9, A23, A24, MATRPROB:20
.=
Sum (M . 1)
by A25, MATRIX_0:60
.=
(Sum p) . 1
by A2, A15, A26, MATRPROB:def 1
;
hence
qq . (k + 1) = (Sum p) . (k + 1)
by A23;
verum end; suppose A27:
k >= 1
;
qq . (k + 1) = (Sum p) . (k + 1)A28:
k < len qq
by A19, NAT_1:13;
then A29:
k < len M
by A8, MATRPROB:def 1;
k in Seg (len qq)
by A27, A28, FINSEQ_1:1;
then A30:
k in dom (Sum p)
by A12, FINSEQ_1:def 3;
qq . (k + 1) =
(qq . k) + ((LineSum M) . (k + 1))
by A8, A10, A27, A28
.=
(Sum (p . k)) + ((LineSum M) . (k + 1))
by A13, A17, A27, A28, A30, FINSEQ_1:1, MATRPROB:def 1
.=
(Sum (p . k)) + (Sum (Line (M,(k + 1))))
by A7, A8, A13, A18, MATRPROB:20
.=
(Sum (p . k)) + (Sum (M . (k + 1)))
by A21, MATRIX_0:60
.=
Sum (p . (k + 1))
by A3, A27, A29, Th37
.=
(Sum p) . (k + 1)
by A20, MATRPROB:def 1
;
hence
qq . (k + 1) = (Sum p) . (k + 1)
;
verum end;
end;
A31:
S1[
0 ]
by A13, FINSEQ_1:1;
for
j being
Nat holds
S1[
j]
from NAT_1:sch 2(A31, A16);
hence
for
j being
Nat st
j in dom qq holds
qq . j = (Sum p) . j
;
verum
end; then A32:
qq = Sum p
by A12, FINSEQ_2:9;
len M in Seg (len M)
by A5, FINSEQ_1:3;
then A33:
len M in dom (Sum p)
by A1, A14, FINSEQ_1:def 3;
thus SumAll M =
Sum (LineSum M)
by MATRPROB:def 3
.=
(Sum p) . (len M)
by A11, A32, MATRPROB:def 1
.=
Sum (p . (len M))
by A33, MATRPROB:def 1
;
verum end;