for a being Element of Z_2 holds Sum <*a*> = a by FINSOP_1:11;