let x, z1, z2 be Element of F_Complex; :: thesis: ( z1 in FQ x & z2 in FQ x implies z1 * z2 in FQ x )
assume that
A1: z1 in FQ x and
A2: z2 in FQ x ; :: thesis: z1 * z2 in FQ x
consider f1 being object such that
A3: f1 in dom (hom_Ext_eval (x,F_Rat)) and
A4: z1 = (hom_Ext_eval (x,F_Rat)) . f1 by A1, FUNCT_1:def 3;
consider f2 being object such that
A5: f2 in dom (hom_Ext_eval (x,F_Rat)) and
A6: z2 = (hom_Ext_eval (x,F_Rat)) . f2 by A2, FUNCT_1:def 3;
A7: dom (hom_Ext_eval (x,F_Rat)) = the carrier of (Polynom-Ring F_Rat) by FUNCT_2:def 1;
reconsider g1 = f1, g2 = f2 as Polynomial of F_Rat by A3, A5, POLYNOM3:def 10;
A8: z1 * z2 = (Ext_eval (g1,x)) * ((hom_Ext_eval (x,F_Rat)) . f2) by Def9, A6, A4
.= (Ext_eval (g1,x)) * (Ext_eval (g2,x)) by Def9
.= Ext_eval ((g1 *' g2),x) by Th3, Th24
.= (hom_Ext_eval (x,F_Rat)) . (g1 *' g2) by Def9 ;
set g = g1 *' g2;
g1 *' g2 in dom (hom_Ext_eval (x,F_Rat)) by A7, POLYNOM3:def 10;
hence z1 * z2 in FQ x by A8, FUNCT_1:def 3; :: thesis: verum