let z, w be G_INTEG; :: thesis: g_int_add . (z,w) = z + w
( z in G_INT_SET & w in G_INT_SET ) ;
hence g_int_add . (z,w) = addcomplex . (z,w) by FUNCT_1:49, ZFMISC_1:87
.= z + w by BINOP_2:def 3 ;
:: thesis: verum