let r be Real; :: thesis: Sum <*r*> = r
reconsider r = r as Element of REAL by XREAL_0:def 1;
Sum <*r*> = r by FINSOP_1:11;
hence Sum <*r*> = r ; :: thesis: verum