let z, w be G_INTEG; :: thesis: g_int_mult . (z,w) = z * w
( z in G_INT_SET & w in G_INT_SET ) ;
hence g_int_mult . (z,w) = multcomplex . (z,w) by FUNCT_1:49, ZFMISC_1:87
.= z * w by BINOP_2:def 5 ;
:: thesis: verum