theorem Lm57: :: ALGNUM_1:46

for x being Element of F_Complex holds the addF of F_Rat = the addF of (FQ_Ring x) || RAT