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

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

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

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

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

len <*x1,x2*> = 2 by FINSEQ_1:44;

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

.= x1 + x2 by RVSUM_1:77 ;

:: thesis: verum

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

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

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

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

len <*x1,x2*> = 2 by FINSEQ_1:44;

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

.= x1 + x2 by RVSUM_1:77 ;

:: thesis: verum