theorem :: GR_CY_1:1

for i1 being Element of INT st i1 = 0 holds
i1 is_a_unity_wrt addint by BINOP_2:4, SETWISEO:14;