theorem Th3: :: GR_CY_1:3

Sum (<*> INT) = 0 by BINOP_2:4, FINSOP_1:10;