let z be G_RAT; :: thesis: for i being Element of RAT holds RSc_Mult . (i,z) = i * z
let i be Element of RAT ; :: thesis: RSc_Mult . (i,z) = i * z
( i in RAT & z in G_RAT_SET ) ;
hence RSc_Mult . (i,z) = multcomplex . (i,z) by FUNCT_1:49, ZFMISC_1:87
.= i * z by BINOP_2:def 5 ;
:: thesis: verum