let x be Element of F_Complex; :: thesis: for z, w being Element of FQ x holds (FQ_mult x) . (z,w) = z * w
let z, w be Element of FQ x; :: thesis: (FQ_mult x) . (z,w) = z * w
thus (FQ_mult x) . (z,w) = multcomplex . (z,w) by FUNCT_1:49, ZFMISC_1:87
.= z * w by BINOP_2:def 5 ; :: thesis: verum