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:5
.= x1 by FINSOP_1:12 ; :: 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:61;
hence Sum (Prefix <*x1,x2*>,2) = Sum <*y1,y2*> by FINSEQ_3:55
.= x1 + x2 by RVSUM_1:107 ;
:: thesis: verum