A1:
for p being FinSequence of REAL holds SumAll <*p*> = SumAll (<*p*> @ )
proof
let p be
FinSequence of
REAL ;
:: thesis: SumAll <*p*> = SumAll (<*p*> @ )
defpred S1[
FinSequence of
REAL ]
means SumAll <*$1*> = SumAll (<*$1*> @ );
A2:
S1[
<*> REAL ]
A4:
for
p being
FinSequence of
REAL for
x being
Element of
REAL st
S1[
p] holds
S1[
p ^ <*x*>]
proof
let p be
FinSequence of
REAL ;
:: thesis: for x being Element of REAL st S1[p] holds
S1[p ^ <*x*>]let x be
Element of
REAL ;
:: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A5:
SumAll <*p*> = SumAll (<*p*> @ )
;
:: thesis: S1[p ^ <*x*>]
Seg (len (<*p*> ^^ <*<*x*>*>)) =
dom (<*p*> ^^ <*<*x*>*>)
by FINSEQ_1:def 3
.=
(dom <*p*>) /\ (dom <*<*x*>*>)
by MATRLIN:def 2
.=
(Seg 1) /\ (dom <*<*x*>*>)
by FINSEQ_1:55
.=
(Seg 1) /\ (Seg 1)
by FINSEQ_1:55
.=
Seg 1
;
then A6:
len (<*p*> ^^ <*<*x*>*>) =
1
by FINSEQ_1:8
.=
len <*(p ^ <*x*>)*>
by FINSEQ_1:56
;
X:
dom <*(p ^ <*x*>)*> = Seg (len <*(p ^ <*x*>)*>)
by FINSEQ_1:def 3;
A7:
now let i be
Nat;
:: thesis: ( i in dom <*(p ^ <*x*>)*> implies (<*p*> ^^ <*<*x*>*>) . i = <*(p ^ <*x*>)*> . i )assume A8:
i in dom <*(p ^ <*x*>)*>
;
:: thesis: (<*p*> ^^ <*<*x*>*>) . i = <*(p ^ <*x*>)*> . ithen A9:
i in dom (<*p*> ^^ <*<*x*>*>)
by A6, X, FINSEQ_1:def 3;
i in {1}
by A8, X, FINSEQ_1:4, FINSEQ_1:57;
then A10:
i = 1
by TARSKI:def 1;
reconsider M1 =
<*p*> . i,
M2 =
<*<*x*>*> . i as
FinSequence ;
thus (<*p*> ^^ <*<*x*>*>) . i =
M1 ^ M2
by A9, MATRLIN:def 2
.=
p ^ M2
by A10, FINSEQ_1:57
.=
p ^ <*x*>
by A10, FINSEQ_1:57
.=
<*(p ^ <*x*>)*> . i
by A10, FINSEQ_1:57
;
:: thesis: verum end;
per cases
( len p = 0 or len p <> 0 )
;
suppose
len p <> 0
;
:: thesis: S1[p ^ <*x*>]then A12:
len p > 0
;
A13:
len <*p*> = 1
by FINSEQ_1:57;
then A14:
width <*p*> = len p
by MATRIX_1:20;
A15:
len <*<*x*>*> = 1
by FINSEQ_1:57;
then A16:
width <*<*x*>*> =
len <*x*>
by MATRIX_1:20
.=
1
by FINSEQ_1:57
;
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:
width (<*p*> @ ) =
len <*p*>
by A12, A14, MATRIX_2:12
.=
width (<*<*x*>*> @ )
by A13, A15, A16, MATRIX_2:12
;
A20:
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 A14, A16, A18, MATRIX_1:def 7
;
A21:
len (<*p*> @ ) = len p
by A14, MATRIX_1:def 7;
width (<*p*> @ ) = 1
by A12, A13, A14, MATRIX_2:12;
then reconsider d1 =
<*p*> @ as
Matrix of
len p,1,
REAL by A12, A21, MATRIX_1:20;
A22:
len (<*<*x*>*> @ ) = 1
by A16, MATRIX_1:def 7;
width (<*<*x*>*> @ ) = 1
by A12, A13, A14, A19, MATRIX_2:12;
then reconsider d2 =
<*<*x*>*> @ as
Matrix of 1,1,
REAL by A22, MATRIX_1:20;
A23:
(<*<*x*>*> @ ) @ = <*<*x*>*>
by A15, A16, MATRIX_2:15;
A24:
(d1 ^ d2) @ =
((<*p*> @ ) @ ) ^^ ((<*<*x*>*> @ ) @ )
by A19, MATRLIN:32
.=
<*p*> ^^ <*<*x*>*>
by A12, A13, A14, A23, MATRIX_2:15
.=
<*(p ^ <*x*>)*>
by A6, A7, FINSEQ_2:10
.=
(<*(p ^ <*x*>)*> @ ) @
by A17, A18, MATRIX_2:15
;
thus SumAll <*(p ^ <*x*>)*> =
SumAll (<*p*> ^^ <*<*x*>*>)
by A6, A7, FINSEQ_2:10
.=
(SumAll (<*p*> @ )) + (SumAll <*<*x*>*>)
by A5, A13, A15, 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 A20, A24, MATRIX_2:11
;
:: thesis: verum end;
end;
for
p being
FinSequence of
REAL holds
S1[
p]
from FINSEQ_2:sch 2(A2, A4);
hence
SumAll <*p*> = SumAll (<*p*> @ )
;
:: thesis: verum
end;
defpred S1[ Nat] means for M being Matrix of REAL st len M = $1 holds
SumAll M = SumAll (M @ );
A25:
S1[ 0 ]
A28:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A29:
for
M being
Matrix of
REAL st
len M = n holds
SumAll M = SumAll (M @ )
;
:: thesis: S1[n + 1]
thus
for
M being
Matrix of
REAL st
len M = n + 1 holds
SumAll M = SumAll (M @ )
:: thesis: verumproof
let M be
Matrix of
REAL ;
:: thesis: ( len M = n + 1 implies SumAll M = SumAll (M @ ) )
assume A30:
len M = n + 1
;
:: thesis: SumAll M = SumAll (M @ )
A31:
dom M = Seg (len M)
by FINSEQ_1:def 3;
per cases
( n = 0 or n > 0 )
;
suppose A33:
n > 0
;
:: thesis: SumAll M = SumAll (M @ )A34:
len (Del M,(n + 1)) = n
by A30, MATRLIN:3;
A35:
M . (n + 1) = Line M,
(n + 1)
by A30, A31, FINSEQ_1:6, MATRIX_2:18;
reconsider M1 =
M . (n + 1) as
FinSequence of
REAL ;
reconsider M' =
M as
Matrix of
n + 1,
width M,
REAL by A30, MATRIX_1:20;
reconsider r =
<*M1*> as
Matrix of 1,
width M,
REAL by A35, MATRIX_1:def 8;
reconsider w =
Del M',
(n + 1) as
Matrix of
n,
width M,
REAL by MATRLIN:5;
A36:
width w =
width M'
by A33, MATRLIN:4
.=
width r
by MATRLIN:4
;
A37:
len (w @ ) =
width w
by MATRIX_1:def 7
.=
len (r @ )
by A36, MATRIX_1:def 7
;
thus SumAll M =
SumAll (w ^ r)
by A30, MATRLIN:6
.=
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 A29, A34
.=
(SumAll ((Del M,(n + 1)) @ )) + (SumAll (r @ ))
by A1
.=
SumAll ((w @ ) ^^ (r @ ))
by A37, Th27
.=
SumAll ((w ^ r) @ )
by A36, MATRLIN:32
.=
SumAll (M @ )
by A30, MATRLIN:6
;
:: thesis: verum end;
end;
end;
let M be Matrix of REAL ; :: thesis: SumAll M = SumAll (M @ )
for n being Nat holds S1[n]
from NAT_1:sch 2(A25, A28);
then
S1[ len M]
;
hence
SumAll M = SumAll (M @ )
; :: thesis: verum