let f be FinSequence of NAT ; :: thesis: 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 ; :: thesis: ( len f >= 1 implies ( Sum (Prefix (<*s*> ^ f),1) = s & Sum (Prefix (<*s*> ^ f),2) = s + (f /. 1) ) )
assume A1: len f >= 1 ; :: thesis: ( Sum (Prefix (<*s*> ^ f),1) = s & Sum (Prefix (<*s*> ^ f),2) = s + (f /. 1) )
set g = <*s*>;
set h = <*s*> ^ f;
A2: (<*s*> ^ f) . 1 = s by FINSEQ_1:58;
A3: len <*s*> = 1 by FINSEQ_1:56;
A4: f /. 1 = f . 1 by A1, FINSEQ_4:24
.= (<*s*> ^ f) . (1 + 1) by A1, A3, FINSEQ_7:3 ;
A5: Seg 1 = dom <*s*> by A3, FINSEQ_1:def 3;
consider n being Nat such that
A6: len f = 1 + n by A1, NAT_1:10;
len (<*s*> ^ f) = 1 + (len f) by A3, FINSEQ_1:35
.= 2 + n by A6 ;
then consider p2, q2 being FinSequence of NAT such that
A7: ( len p2 = 2 & len q2 = n & <*s*> ^ f = p2 ^ q2 ) by FINSEQ_2:26;
Seg 2 = dom p2 by A7, FINSEQ_1:def 3;
then A8: p2 = Prefix (<*s*> ^ f),2 by A7, FINSEQ_1:33;
reconsider x1 = s as Element of INT by INT_1:def 2;
thus Sum (Prefix (<*s*> ^ f),1) = Sum <*x1*> by A5, FINSEQ_1:33
.= s by FINSOP_1:12 ; :: thesis: Sum (Prefix (<*s*> ^ f),2) = s + (f /. 1)
reconsider x2 = f /. 1 as Element of INT by INT_1:def 2;
A9: p2 . 1 = s by A2, A7, FINSEQ_1:85;
p2 . 2 = f /. 1 by A4, A7, FINSEQ_1:85;
hence Sum (Prefix (<*s*> ^ f),2) = Sum <*x1,x2*> by A7, A8, A9, FINSEQ_1:61
.= s + (f /. 1) by RVSUM_1:107 ;
:: thesis: verum