let x be Element of F_Complex; :: thesis: the multF of F_Rat = the multF of (FQ_Ring x) || RAT
thus the multF of F_Rat = multcomplex | [:RAT,RAT:] by ZFMISC_1:96, RELAT_1:74, VECTSP_1:def 5, RING_3:3, GAUSSINT:13
.= the multF of (FQ_Ring x) || RAT by Lm56, RELAT_1:74 ; :: thesis: verum