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