for R being Element of 0 -tuples_on REAL holds Sum R = 0 by Th72;