let f be FinSequence of NAT ; for s being Element of NAT st len f >= 1 holds
( Sum (Prefix ((<*s*> ^ f),1)) = s & Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1) )
let s be Element of NAT ; ( len f >= 1 implies ( Sum (Prefix ((<*s*> ^ f),1)) = s & Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1) ) )
set g = <*s*>;
set h = <*s*> ^ f;
reconsider x1 = s as Element of INT by INT_1:def 2;
reconsider x2 = f /. 1 as Element of INT by INT_1:def 2;
assume A1:
len f >= 1
; ( Sum (Prefix ((<*s*> ^ f),1)) = s & Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1) )
then consider n being Nat such that
A2:
len f = 1 + n
by NAT_1:10;
A3:
len <*s*> = 1
by FINSEQ_1:39;
then
Seg 1 = dom <*s*>
by FINSEQ_1:def 3;
hence Sum (Prefix ((<*s*> ^ f),1)) =
Sum <*x1*>
by FINSEQ_1:21
.=
s
by FINSOP_1:11
;
Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1)
len (<*s*> ^ f) =
1 + (len f)
by A3, FINSEQ_1:22
.=
2 + n
by A2
;
then consider p2, q2 being FinSequence of NAT such that
A4:
len p2 = 2
and
len q2 = n
and
A5:
<*s*> ^ f = p2 ^ q2
by FINSEQ_2:23;
f /. 1 =
f . 1
by A1, FINSEQ_4:15
.=
(<*s*> ^ f) . (1 + 1)
by A1, A3, FINSEQ_7:3
;
then A6:
p2 . 2 = f /. 1
by A4, A5, FINSEQ_1:64;
Seg 2 = dom p2
by A4, FINSEQ_1:def 3;
then A7:
p2 = Prefix ((<*s*> ^ f),2)
by A5, FINSEQ_1:21;
(<*s*> ^ f) . 1 = s
by FINSEQ_1:41;
then
p2 . 1 = s
by A4, A5, FINSEQ_1:64;
hence Sum (Prefix ((<*s*> ^ f),2)) =
Sum <*x1,x2*>
by A4, A7, A6, FINSEQ_1:44
.=
s + (f /. 1)
by RVSUM_1:77
;
verum