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) ) )

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;

reconsider x3 = f /. 2 as Element of INT by INT_1:def 2;

reconsider x4 = f /. 3 as Element of INT by INT_1:def 2;

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) )

then consider n being Nat such that

A2: len f = 3 + n by NAT_1:10;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A3: len <*s*> = 1 by FINSEQ_1:39;

then A4: len (<*s*> ^ f) = 1 + (len f) by FINSEQ_1:22

.= 4 + n by A2 ;

then consider p4, q4 being FinSequence of NAT such that

A5: len p4 = 4 and

len q4 = n and

A6: <*s*> ^ f = p4 ^ q4 by FINSEQ_2:23;

f /. 3 = f . 3 by A1, FINSEQ_4:15

.= (<*s*> ^ f) . (1 + 3) by A1, A3, FINSEQ_7:3 ;

then A7: p4 . 4 = f /. 3 by A5, A6, FINSEQ_1:64;

Seg 4 = dom p4 by A5, FINSEQ_1:def 3;

then A8: p4 = Prefix ((<*s*> ^ f),4) by A6, FINSEQ_1:21;

A9: 1 <= len f by A1, XXREAL_0:2;

hence ( Sum (Prefix ((<*s*> ^ f),1)) = s & Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1) ) by Th20; :: thesis: ( Sum (Prefix ((<*s*> ^ f),3)) = (s + (f /. 1)) + (f /. 2) & Sum (Prefix ((<*s*> ^ f),4)) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3) )

len (<*s*> ^ f) = 3 + (1 + n) by A4;

then consider p3, q3 being FinSequence of NAT such that

A10: len p3 = 3 and

len q3 = 1 + n and

A11: <*s*> ^ f = p3 ^ q3 by FINSEQ_2:23;

A12: f /. 1 = f . 1 by A9, FINSEQ_4:15

.= (<*s*> ^ f) . (1 + 1) by A9, A3, FINSEQ_7:3 ;

then A13: p4 . 2 = f /. 1 by A5, A6, FINSEQ_1:64;

A14: 2 <= len f by A1, XXREAL_0:2;

then A15: f /. 2 = f . 2 by FINSEQ_4:15

.= (<*s*> ^ f) . (1 + 2) by A3, A14, FINSEQ_7:3 ;

then A16: p4 . 3 = f /. 2 by A5, A6, FINSEQ_1:64;

A17: p3 . 2 = f /. 1 by A12, A10, A11, FINSEQ_1:64;

Seg 3 = dom p3 by A10, FINSEQ_1:def 3;

then A18: p3 = Prefix ((<*s*> ^ f),3) by A11, FINSEQ_1:21;

A19: p3 . 3 = f /. 2 by A15, A10, A11, FINSEQ_1:64;

A20: (<*s*> ^ f) . 1 = s by FINSEQ_1:41;

then p3 . 1 = s by A10, A11, FINSEQ_1:64;

then p3 = <*s,(f /. 1),(f /. 2)*> by A10, A17, A19, FINSEQ_1:45;

hence Sum (Prefix ((<*s*> ^ f),3)) = (s + (f /. 1)) + (f /. 2) by A18, RVSUM_1:78; :: thesis: Sum (Prefix ((<*s*> ^ f),4)) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3)

p4 . 1 = s by A20, A5, A6, FINSEQ_1:64;

then p4 = <*s,(f /. 1),(f /. 2),(f /. 3)*> by A5, A13, A16, A7, FINSEQ_4:76;

hence Sum (Prefix ((<*s*> ^ f),4)) = ((x1 + x2) + x3) + x4 by A8, RVSUM_1:142

.= ((s + (f /. 1)) + (f /. 2)) + (f /. 3) ;

:: thesis: verum

( 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) ) )

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;

reconsider x3 = f /. 2 as Element of INT by INT_1:def 2;

reconsider x4 = f /. 3 as Element of INT by INT_1:def 2;

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) )

then consider n being Nat such that

A2: len f = 3 + n by NAT_1:10;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A3: len <*s*> = 1 by FINSEQ_1:39;

then A4: len (<*s*> ^ f) = 1 + (len f) by FINSEQ_1:22

.= 4 + n by A2 ;

then consider p4, q4 being FinSequence of NAT such that

A5: len p4 = 4 and

len q4 = n and

A6: <*s*> ^ f = p4 ^ q4 by FINSEQ_2:23;

f /. 3 = f . 3 by A1, FINSEQ_4:15

.= (<*s*> ^ f) . (1 + 3) by A1, A3, FINSEQ_7:3 ;

then A7: p4 . 4 = f /. 3 by A5, A6, FINSEQ_1:64;

Seg 4 = dom p4 by A5, FINSEQ_1:def 3;

then A8: p4 = Prefix ((<*s*> ^ f),4) by A6, FINSEQ_1:21;

A9: 1 <= len f by A1, XXREAL_0:2;

hence ( Sum (Prefix ((<*s*> ^ f),1)) = s & Sum (Prefix ((<*s*> ^ f),2)) = s + (f /. 1) ) by Th20; :: thesis: ( Sum (Prefix ((<*s*> ^ f),3)) = (s + (f /. 1)) + (f /. 2) & Sum (Prefix ((<*s*> ^ f),4)) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3) )

len (<*s*> ^ f) = 3 + (1 + n) by A4;

then consider p3, q3 being FinSequence of NAT such that

A10: len p3 = 3 and

len q3 = 1 + n and

A11: <*s*> ^ f = p3 ^ q3 by FINSEQ_2:23;

A12: f /. 1 = f . 1 by A9, FINSEQ_4:15

.= (<*s*> ^ f) . (1 + 1) by A9, A3, FINSEQ_7:3 ;

then A13: p4 . 2 = f /. 1 by A5, A6, FINSEQ_1:64;

A14: 2 <= len f by A1, XXREAL_0:2;

then A15: f /. 2 = f . 2 by FINSEQ_4:15

.= (<*s*> ^ f) . (1 + 2) by A3, A14, FINSEQ_7:3 ;

then A16: p4 . 3 = f /. 2 by A5, A6, FINSEQ_1:64;

A17: p3 . 2 = f /. 1 by A12, A10, A11, FINSEQ_1:64;

Seg 3 = dom p3 by A10, FINSEQ_1:def 3;

then A18: p3 = Prefix ((<*s*> ^ f),3) by A11, FINSEQ_1:21;

A19: p3 . 3 = f /. 2 by A15, A10, A11, FINSEQ_1:64;

A20: (<*s*> ^ f) . 1 = s by FINSEQ_1:41;

then p3 . 1 = s by A10, A11, FINSEQ_1:64;

then p3 = <*s,(f /. 1),(f /. 2)*> by A10, A17, A19, FINSEQ_1:45;

hence Sum (Prefix ((<*s*> ^ f),3)) = (s + (f /. 1)) + (f /. 2) by A18, RVSUM_1:78; :: thesis: Sum (Prefix ((<*s*> ^ f),4)) = ((s + (f /. 1)) + (f /. 2)) + (f /. 3)

p4 . 1 = s by A20, A5, A6, FINSEQ_1:64;

then p4 = <*s,(f /. 1),(f /. 2),(f /. 3)*> by A5, A13, A16, A7, FINSEQ_4:76;

hence Sum (Prefix ((<*s*> ^ f),4)) = ((x1 + x2) + x3) + x4 by A8, RVSUM_1:142

.= ((s + (f /. 1)) + (f /. 2)) + (f /. 3) ;

:: thesis: verum