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