thus (hom_Ext_eval (x,F_Rat)) . (1_ (Polynom-Ring F_Rat)) = (hom_Ext_eval (x,F_Rat)) . (1_. F_Rat) by POLYNOM3:37
.= Ext_eval ((1_. F_Rat),x) by Def9
.= 1_ F_Complex by Th3, Th18 ; :: according to GROUP_1:def 13 :: thesis: ( hom_Ext_eval (x,F_Rat) is additive & hom_Ext_eval (x,F_Rat) is multiplicative )

hereby :: according to VECTSP_1:def 19 :: thesis: hom_Ext_eval (x,F_Rat) is multiplicative

let a, b be Element of (Polynom-Ring F_Rat); :: thesis: (hom_Ext_eval (x,F_Rat)) . (a + b) = ((hom_Ext_eval (x,F_Rat)) . a) + ((hom_Ext_eval (x,F_Rat)) . b)
reconsider p = a, q = b as Polynomial of F_Rat by POLYNOM3:def 10;
thus (hom_Ext_eval (x,F_Rat)) . (a + b) = (hom_Ext_eval (x,F_Rat)) . (p + q) by POLYNOM3:def 10
.= Ext_eval ((p + q),x) by Def9
.= (Ext_eval (p,x)) + (Ext_eval (q,x)) by Th3, Th19
.= ((hom_Ext_eval (x,F_Rat)) . a) + (Ext_eval (q,x)) by Def9
.= ((hom_Ext_eval (x,F_Rat)) . a) + ((hom_Ext_eval (x,F_Rat)) . b) by Def9 ; :: thesis: verum

end;

hereby :: according to GROUP_6:def 6 :: thesis: verum

let a, b be Element of (Polynom-Ring F_Rat); :: thesis: (hom_Ext_eval (x,F_Rat)) . (a * b) = ((hom_Ext_eval (x,F_Rat)) . a) * ((hom_Ext_eval (x,F_Rat)) . b)
reconsider p = a, q = b as Polynomial of F_Rat by POLYNOM3:def 10;
thus (hom_Ext_eval (x,F_Rat)) . (a * b) = (hom_Ext_eval (x,F_Rat)) . (p *' q) by POLYNOM3:def 10
.= Ext_eval ((p *' q),x) by Def9
.= (Ext_eval (p,x)) * (Ext_eval (q,x)) by Th3, Th24
.= ((hom_Ext_eval (x,F_Rat)) . a) * (Ext_eval (q,x)) by Def9
.= ((hom_Ext_eval (x,F_Rat)) . a) * ((hom_Ext_eval (x,F_Rat)) . b) by Def9 ; :: thesis: verum

end;