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