let M be Matrix of REAL; SumAll M = SumAll (M @)
defpred S1[ Nat] means for M being Matrix of REAL st len M = $1 holds
SumAll M = SumAll (M @);
A1:
for p being FinSequence of REAL holds SumAll <*p*> = SumAll (<*p*> @)
proof
defpred S2[
FinSequence of
REAL ]
means SumAll <*$1*> = SumAll (<*$1*> @);
let p be
FinSequence of
REAL ;
SumAll <*p*> = SumAll (<*p*> @)
A2:
for
p being
FinSequence of
REAL for
x being
Element of
REAL st
S2[
p] holds
S2[
p ^ <*x*>]
proof
let p be
FinSequence of
REAL ;
for x being Element of REAL st S2[p] holds
S2[p ^ <*x*>]let x be
Element of
REAL ;
( S2[p] implies S2[p ^ <*x*>] )
assume A3:
SumAll <*p*> = SumAll (<*p*> @)
;
S2[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:55
.=
(Seg 1) /\ (Seg 1)
by FINSEQ_1:55
.=
Seg 1
;
then A4:
len (<*p*> ^^ <*<*x*>*>) =
1
by FINSEQ_1:8
.=
len <*(p ^ <*x*>)*>
by FINSEQ_1:56
;
A5:
dom <*(p ^ <*x*>)*> = Seg (len <*(p ^ <*x*>)*>)
by FINSEQ_1:def 3;
per cases
( len p = 0 or len p <> 0 )
;
suppose A10:
len p <> 0
;
S2[p ^ <*x*>]A11:
len <*<*x*>*> = 1
by FINSEQ_1:57;
then A12:
width <*<*x*>*> =
len <*x*>
by MATRIX_1:20
.=
1
by FINSEQ_1:57
;
then A13:
len (<*<*x*>*> @) = 1
by MATRIX_1:def 7;
A14:
len <*p*> = 1
by FINSEQ_1:57;
then A15:
width <*p*> = len p
by MATRIX_1:20;
then A16:
len (<*p*> @) = len p
by MATRIX_1:def 7;
width (<*p*> @) = 1
by A10, A14, A15, MATRIX_2:12;
then reconsider d1 =
<*p*> @ as
Matrix of
len p,1,
REAL by A10, A16, MATRIX_1:20;
A17:
len <*(p ^ <*x*>)*> = 1
by FINSEQ_1:57;
then A18:
width <*(p ^ <*x*>)*> =
len (p ^ <*x*>)
by MATRIX_1:20
.=
(len p) + (len <*x*>)
by FINSEQ_1:35
.=
(len p) + 1
by FINSEQ_1:57
;
A19:
(<*<*x*>*> @) @ = <*<*x*>*>
by A11, A12, MATRIX_2:15;
A20:
width (<*p*> @) =
len <*p*>
by A10, A15, MATRIX_2:12
.=
width (<*<*x*>*> @)
by A14, A11, A12, MATRIX_2:12
;
then
width (<*<*x*>*> @) = 1
by A10, A14, A15, MATRIX_2:12;
then reconsider d2 =
<*<*x*>*> @ as
Matrix of 1,1,
REAL by A13, MATRIX_1:20;
A21:
(d1 ^ d2) @ =
((<*p*> @) @) ^^ ((<*<*x*>*> @) @)
by A20, MATRLIN:32
.=
<*p*> ^^ <*<*x*>*>
by A10, A14, A15, A19, MATRIX_2:15
.=
<*(p ^ <*x*>)*>
by A4, A6, FINSEQ_2:10
.=
(<*(p ^ <*x*>)*> @) @
by A17, A18, MATRIX_2:15
;
A22:
len ((<*p*> @) ^ (<*<*x*>*> @)) =
(len (<*p*> @)) + (len (<*<*x*>*> @))
by FINSEQ_1:35
.=
(width <*p*>) + (len (<*<*x*>*> @))
by MATRIX_1:def 7
.=
(width <*p*>) + (width <*<*x*>*>)
by MATRIX_1:def 7
.=
len (<*(p ^ <*x*>)*> @)
by A15, A12, A18, MATRIX_1:def 7
;
thus SumAll <*(p ^ <*x*>)*> =
SumAll (<*p*> ^^ <*<*x*>*>)
by A4, A6, FINSEQ_2:10
.=
(SumAll (<*p*> @)) + (SumAll <*<*x*>*>)
by A3, A14, A11, Th27
.=
(SumAll (<*p*> @)) + (SumAll (<*<*x*>*> @))
by MATRLIN:19
.=
Sum ((Sum d1) ^ (Sum d2))
by RVSUM_1:105
.=
SumAll (d1 ^ d2)
by Th25
.=
SumAll (<*(p ^ <*x*>)*> @)
by A22, A21, MATRIX_2:11
;
verum end;
end;
A23:
S2[
<*> REAL]
for
p being
FinSequence of
REAL holds
S2[
p]
from FINSEQ_2:sch 2(A23, A2);
hence
SumAll <*p*> = SumAll (<*p*> @)
;
verum
end;
A25:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A26:
for
M being
Matrix of
REAL st
len M = n holds
SumAll M = SumAll (M @)
;
S1[n + 1]
thus
for
M being
Matrix of
REAL st
len M = n + 1 holds
SumAll M = SumAll (M @)
verumproof
let M be
Matrix of
REAL;
( len M = n + 1 implies SumAll M = SumAll (M @) )
assume A27:
len M = n + 1
;
SumAll M = SumAll (M @)
A28:
dom M = Seg (len M)
by FINSEQ_1:def 3;
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,
REAL by A27, MATRIX_1:20;
reconsider M1 =
M . (n + 1) as
FinSequence of
REAL ;
reconsider w =
Del (
M9,
(n + 1)) as
Matrix of
n,
width M,
REAL by MATRLIN:5;
M . (n + 1) = Line (
M,
(n + 1))
by A27, A28, FINSEQ_1:6, MATRIX_2:18;
then reconsider r =
<*M1*> as
Matrix of 1,
width M,
REAL by MATRIX_1:def 8;
A31:
width w =
width M9
by A30, MATRLIN:4
.=
width r
by MATRLIN:4
;
A32:
len (w @) =
width w
by MATRIX_1:def 7
.=
len (r @)
by A31, MATRIX_1:def 7
;
A33:
len (Del (M,(n + 1))) = n
by A27, PRE_POLY:12;
thus SumAll M =
SumAll (w ^ r)
by A27, PRE_POLY:13
.=
Sum ((Sum w) ^ (Sum r))
by Th25
.=
(SumAll (Del (M,(n + 1)))) + (SumAll r)
by RVSUM_1:105
.=
(SumAll ((Del (M,(n + 1))) @)) + (SumAll r)
by A26, A33
.=
(SumAll ((Del (M,(n + 1))) @)) + (SumAll (r @))
by A1
.=
SumAll ((w @) ^^ (r @))
by A32, Th27
.=
SumAll ((w ^ r) @)
by A31, MATRLIN:32
.=
SumAll (M @)
by A27, PRE_POLY:13
;
verum end;
end;
end;
A34:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A34, A25);
then
S1[ len M]
;
hence
SumAll M = SumAll (M @)
; verum