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

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 ; :: thesis: ( 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 ;

:: thesis: 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 ;

:: thesis: verum

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

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 ; :: thesis: ( 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 ;

:: thesis: 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 ;

:: thesis: verum