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