let x be Element of F_Complex; ( [: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; verum