(1. Z_2 ) + (1. Z_2 ) = (1 + 1) mod 2 by Th6, GR_CY_1:def 5
.= 0 by NAT_D:25 ;
hence (1. Z_2 ) + (1. Z_2 ) = 0. Z_2 by FUNCT_7:def 1; :: thesis: verum