let x1, x2, x3 be Element of NAT ; :: thesis: ( Sum (Prefix (<*x1,x2,x3*>,1)) = x1 & Sum (Prefix (<*x1,x2,x3*>,2)) = x1 + x2 & Sum (Prefix (<*x1,x2,x3*>,3)) = (x1 + x2) + x3 )

reconsider y1 = x1 as Element of INT by INT_1:def 2;

thus Sum (Prefix (<*x1,x2,x3*>,1)) = Sum <*y1*> by FINSEQ_6:4

.= x1 by FINSOP_1:11 ; :: thesis: ( Sum (Prefix (<*x1,x2,x3*>,2)) = x1 + x2 & Sum (Prefix (<*x1,x2,x3*>,3)) = (x1 + x2) + x3 )

reconsider y2 = x2 as Element of INT by INT_1:def 2;

thus Sum (Prefix (<*x1,x2,x3*>,2)) = Sum <*y1,y2*> by FINSEQ_6:5

.= x1 + x2 by RVSUM_1:77 ; :: thesis: Sum (Prefix (<*x1,x2,x3*>,3)) = (x1 + x2) + x3

reconsider y3 = x3 as Element of INT by INT_1:def 2;

len <*x1,x2,x3*> = 3 by FINSEQ_1:45;

hence Sum (Prefix (<*x1,x2,x3*>,3)) = Sum <*y1,y2,y3*> by FINSEQ_3:49

.= (x1 + x2) + x3 by RVSUM_1:78 ;

:: thesis: verum

reconsider y1 = x1 as Element of INT by INT_1:def 2;

thus Sum (Prefix (<*x1,x2,x3*>,1)) = Sum <*y1*> by FINSEQ_6:4

.= x1 by FINSOP_1:11 ; :: thesis: ( Sum (Prefix (<*x1,x2,x3*>,2)) = x1 + x2 & Sum (Prefix (<*x1,x2,x3*>,3)) = (x1 + x2) + x3 )

reconsider y2 = x2 as Element of INT by INT_1:def 2;

thus Sum (Prefix (<*x1,x2,x3*>,2)) = Sum <*y1,y2*> by FINSEQ_6:5

.= x1 + x2 by RVSUM_1:77 ; :: thesis: Sum (Prefix (<*x1,x2,x3*>,3)) = (x1 + x2) + x3

reconsider y3 = x3 as Element of INT by INT_1:def 2;

len <*x1,x2,x3*> = 3 by FINSEQ_1:45;

hence Sum (Prefix (<*x1,x2,x3*>,3)) = Sum <*y1,y2,y3*> by FINSEQ_3:49

.= (x1 + x2) + x3 by RVSUM_1:78 ;

:: thesis: verum