let g be Element of (INT.Group 2); :: thesis: ( g = 1 implies g * g = 1_ (INT.Group 2) )
assume A1: g = 1 ; :: thesis: g * g = 1_ (INT.Group 2)
g in the carrier of (INT.Group 2) ;
then A2: 1 in Segm 2 by A1, Th76;
thus g * g = (addint 2) . (g,g) by Th75
.= (1 + 1) mod 2 by A1, A2, GR_CY_1:def 4
.= (2 * 1) mod 2
.= 0 by NAT_D:13
.= 1_ (INT.Group 2) by GR_CY_1:14 ; :: thesis: verum