let z be G_INTEG; :: thesis: for i being Integer holds Sc_Mult . (i,z) = i * z
let i be Integer; :: thesis: Sc_Mult . (i,z) = i * z
set scmult = Sc_Mult ;
A1: ( i in INT & z in G_INT_SET ) by INT_1:def 2;
the carrier of INT.Ring = INT by INT_3:def 3;
hence Sc_Mult . (i,z) = multcomplex . (i,z) by A1, FUNCT_1:49, ZFMISC_1:87
.= i * z by BINOP_2:def 5 ;
:: thesis: verum