let i1, i2, i3, i4 be Element of INT ; :: thesis: Sum <*i1,i2,i3,i4*> = ((i1 + i2) + i3) + i4
thus Sum <*i1,i2,i3,i4*> = Sum (<*i1,i2,i3*> ^ <*i4*>) by FINSEQ_4:def 8
.= (Sum <*i1,i2,i3*>) + (@ i4) by GR_CY_1:20
.= ((i1 + i2) + i3) + i4 by RVSUM_1:108 ; :: thesis: verum