let x, z1, z2 be Element of F_Complex; ( 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
; 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, Th19
.=
(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; verum