A1: Z/ 2 = doubleLoopStr(# (Segm 2),(addint 2),(multint 2),(In (1,(Segm 2))),(In (0,(Segm 2))) #) by INT_3:def 12;
1. (Z/ 2) = 1 by INT_3:14;
hence (1. (Z/ 2)) + (1. (Z/ 2)) = (1 + 1) mod 2 by A1, GR_CY_1:def 4
.= 0 by INT_1:50
.= 0. (Z/ 2) by Th4 ;
:: thesis: verum