let f be FinSequence of NAT ; :: thesis: for s being Element of NAT st len f >= 3 holds
( Sum (Prefix (<*s*> ^ f),1) = s & Sum (Prefix (<*s*> ^ f),2) = s + (f /. 1) & Sum (Prefix (<*s*> ^ f),3) = (s + (f /. 1)) + (f /. 2) & Sum (Prefix (<*s*> ^ f),4) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3) )
let s be Element of NAT ; :: thesis: ( len f >= 3 implies ( Sum (Prefix (<*s*> ^ f),1) = s & Sum (Prefix (<*s*> ^ f),2) = s + (f /. 1) & Sum (Prefix (<*s*> ^ f),3) = (s + (f /. 1)) + (f /. 2) & Sum (Prefix (<*s*> ^ f),4) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3) ) )
assume A1: len f >= 3 ; :: thesis: ( Sum (Prefix (<*s*> ^ f),1) = s & Sum (Prefix (<*s*> ^ f),2) = s + (f /. 1) & Sum (Prefix (<*s*> ^ f),3) = (s + (f /. 1)) + (f /. 2) & Sum (Prefix (<*s*> ^ f),4) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3) )
set g = <*s*>;
set h = <*s*> ^ f;
A2: 1 <= len f by A1, XXREAL_0:2;
hence ( Sum (Prefix (<*s*> ^ f),1) = s & Sum (Prefix (<*s*> ^ f),2) = s + (f /. 1) ) by Th23; :: thesis: ( Sum (Prefix (<*s*> ^ f),3) = (s + (f /. 1)) + (f /. 2) & Sum (Prefix (<*s*> ^ f),4) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3) )
A3: (<*s*> ^ f) . 1 = s by FINSEQ_1:58;
A4: len <*s*> = 1 by FINSEQ_1:56;
A5: f /. 1 = f . 1 by A2, FINSEQ_4:24
.= (<*s*> ^ f) . (1 + 1) by A2, A4, FINSEQ_7:3 ;
A6: 2 <= len f by A1, XXREAL_0:2;
then A7: f /. 2 = f . 2 by FINSEQ_4:24
.= (<*s*> ^ f) . (1 + 2) by A4, A6, FINSEQ_7:3 ;
A8: f /. 3 = f . 3 by A1, FINSEQ_4:24
.= (<*s*> ^ f) . (1 + 3) by A1, A4, FINSEQ_7:3 ;
consider n being Nat such that
A9: len f = 3 + n by A1, NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A10: len (<*s*> ^ f) = 1 + (len f) by A4, FINSEQ_1:35
.= 4 + n by A9 ;
then len (<*s*> ^ f) = 3 + (1 + n) ;
then consider p3, q3 being FinSequence of NAT such that
A11: ( len p3 = 3 & len q3 = 1 + n & <*s*> ^ f = p3 ^ q3 ) by FINSEQ_2:26;
Seg 3 = dom p3 by A11, FINSEQ_1:def 3;
then A12: p3 = Prefix (<*s*> ^ f),3 by A11, FINSEQ_1:33;
consider p4, q4 being FinSequence of NAT such that
A13: ( len p4 = 4 & len q4 = n & <*s*> ^ f = p4 ^ q4 ) by A10, FINSEQ_2:26;
Seg 4 = dom p4 by A13, FINSEQ_1:def 3;
then A14: p4 = Prefix (<*s*> ^ f),4 by A13, FINSEQ_1:33;
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;
reconsider x3 = f /. 2 as Element of INT by INT_1:def 2;
A15: p3 . 1 = s by A3, A11, FINSEQ_1:85;
A16: p3 . 2 = f /. 1 by A5, A11, FINSEQ_1:85;
p3 . 3 = f /. 2 by A7, A11, FINSEQ_1:85;
then p3 = <*s,(f /. 1),(f /. 2)*> by A11, A15, A16, FINSEQ_1:62;
hence Sum (Prefix (<*s*> ^ f),3) = (s + (f /. 1)) + (f /. 2) by A12, RVSUM_1:108; :: thesis: Sum (Prefix (<*s*> ^ f),4) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3)
reconsider x4 = f /. 3 as Element of INT by INT_1:def 2;
A17: p4 . 1 = s by A3, A13, FINSEQ_1:85;
A18: p4 . 2 = f /. 1 by A5, A13, FINSEQ_1:85;
A19: p4 . 3 = f /. 2 by A7, A13, FINSEQ_1:85;
p4 . 4 = f /. 3 by A8, A13, FINSEQ_1:85;
then p4 = <*s,(f /. 1),(f /. 2),(f /. 3)*> by A13, A17, A18, A19, FINSEQ_4:91;
hence Sum (Prefix (<*s*> ^ f),4) = ((x1 + x2) + x3) + x4 by A14, Th6
.= ((s + (f /. 1)) + (f /. 2)) + (f /. 3) ;
:: thesis: verum