let L be non empty right_complementable add-associative right_zeroed left_zeroed doubleLoopStr ; for m being Element of NAT
for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) holds
Sum s = m * (1. L)
let m be Element of NAT ; for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) holds
Sum s = m * (1. L)
let s be FinSequence of L; ( len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) implies Sum s = m * (1. L) )
assume A1:
( len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) )
; Sum s = m * (1. L)
defpred S1[ Nat] means for s being FinSequence of L st len s = $1 & ( for k being Element of NAT st 1 <= k & k <= $1 holds
s /. k = 1. L ) holds
Sum s = $1 * (1. L);
A2:
for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be
Nat;
( S1[l] implies S1[l + 1] )
assume A3:
for
g being
FinSequence of
L st
len g = l & ( for
k being
Element of
NAT st 1
<= k &
k <= l holds
g /. k = 1. L ) holds
Sum g = l * (1. L)
;
S1[l + 1]
for
s being
FinSequence of
L st
len s = l + 1 & ( for
k being
Element of
NAT st 1
<= k &
k <= l + 1 holds
s /. k = 1. L ) holds
Sum s = (l + 1) * (1. L)
proof
ex
G being
FinSequence of
L st
(
dom G = Seg l & ( for
k being
Nat st
k in Seg l holds
G . k = 1. L ) )
then consider g being
FinSequence of
L such that A5:
dom g = Seg l
and A6:
for
k being
Nat st
k in Seg l holds
g . k = 1. L
;
A7:
l in NAT
by ORDINAL1:def 12;
then A8:
len g = l
by A5, FINSEQ_1:def 3;
A9:
for
k being
Nat st 1
<= k &
k <= l holds
g /. k = 1. L
then A12:
for
k being
Element of
NAT st 1
<= k &
k <= l holds
g /. k = 1. L
;
dom <*(1. L)*> = Seg 1
by FINSEQ_1:def 8;
then A13:
len <*(1. L)*> = 1
by FINSEQ_1:def 3;
let s be
FinSequence of
L;
( len s = l + 1 & ( for k being Element of NAT st 1 <= k & k <= l + 1 holds
s /. k = 1. L ) implies Sum s = (l + 1) * (1. L) )
assume that A14:
len s = l + 1
and A15:
for
k being
Element of
NAT st 1
<= k &
k <= l + 1 holds
s /. k = 1. L
;
Sum s = (l + 1) * (1. L)
A16:
dom s = Seg (l + 1)
by A14, FINSEQ_1:def 3;
A17:
for
k being
Nat st
k in dom s holds
s . k = (g ^ <*(1. L)*>) . k
proof
A18:
dom s = Seg (l + 1)
by A14, FINSEQ_1:def 3;
let k be
Nat;
( k in dom s implies s . k = (g ^ <*(1. L)*>) . k )
A19:
k in NAT
by ORDINAL1:def 12;
assume A20:
k in dom s
;
s . k = (g ^ <*(1. L)*>) . k
per cases
( ( 1 <= k & k <= l ) or ( l < k & k <= l + 1 ) )
by A20, A18, FINSEQ_1:1;
suppose A24:
(
l < k &
k <= l + 1 )
;
s . k = (g ^ <*(1. L)*>) . kthen
k - k <= (l + 1) - k
by XREAL_1:9;
then reconsider ii =
((l + 1) - k) + 1 as
Element of
NAT by INT_1:3;
l + 1
<= k
by A24, NAT_1:13;
then
(
dom <*(1. L)*> = Seg 1 &
ii = (k - k) + 1 )
by A24, FINSEQ_1:def 8, XXREAL_0:1;
then A25:
ii in dom <*(1. L)*>
;
l + 0 < k + l
by A24, XREAL_1:8;
then
l + 1
<= k + l
by NAT_1:13;
then A26:
(l + 1) - l <= (k + l) - l
by XREAL_1:9;
l + 1
<= k
by A24, NAT_1:13;
then A27:
ii = (k - k) + 1
by A24, XXREAL_0:1;
then (g ^ <*(1. L)*>) . k =
(g ^ <*(1. L)*>) . ((len g) + ii)
by A5, FINSEQ_1:def 3, A7
.=
<*(1. L)*> . 1
by A25, A27, FINSEQ_1:def 7
.=
1. L
by FINSEQ_1:def 8
.=
s /. k
by A15, A19, A24, A26
.=
s . k
by A20, PARTFUN1:def 6
;
hence
s . k = (g ^ <*(1. L)*>) . k
;
verum end; end;
end;
dom (g ^ <*(1. L)*>) =
Seg ((len g) + (len <*(1. L)*>))
by FINSEQ_1:def 7
.=
dom s
by A5, A13, A16, FINSEQ_1:def 3, A7
;
then
s = g ^ <*(1. L)*>
by A17, FINSEQ_1:13;
then Sum s =
(Sum g) + (1. L)
by FVSUM_1:71
.=
(l * (1. L)) + (1. L)
by A3, A8, A12
.=
(l * (1. L)) + (1 * (1. L))
by BINOM:13
.=
(l + 1) * (1. L)
by BINOM:15
;
hence
Sum s = (l + 1) * (1. L)
;
verum
end;
hence
S1[
l + 1]
;
verum
end;
for s being FinSequence of L st len s = 0 & ( for k being Element of NAT st 1 <= k & k <= 0 holds
s /. k = 1. L ) holds
Sum s = 0 * (1. L)
then A30:
S1[ 0 ]
;
for l being Nat holds S1[l]
from NAT_1:sch 2(A30, A2);
hence
Sum s = m * (1. L)
by A1; verum