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