let x be Element of F_Complex; :: thesis: ( [:RAT,RAT:] c= [:(FQ x),(FQ x):] & [:(FQ x),(FQ x):] c= [:COMPLEX,COMPLEX:] )
A1: the carrier of F_Rat c= the carrier of (FQ_Ring x) by Lm48;
A2: FQ x c= the carrier of F_Complex ;
FQ x c= COMPLEX by A2, COMPLFLD:def 1;
hence ( [:RAT,RAT:] c= [:(FQ x),(FQ x):] & [:(FQ x),(FQ x):] c= [:COMPLEX,COMPLEX:] ) by A1, ZFMISC_1:96; :: thesis: verum