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