let a, b be Element of (Polynom-Ring L); :: according to GRCAT_1:def 13 :: thesis: (Polynom-Evaluation L,x) . (a + b) = ((Polynom-Evaluation L,x) . a) + ((Polynom-Evaluation L,x) . b)
reconsider p = a, q = b as Polynomial of L by POLYNOM3:def 12;
thus (Polynom-Evaluation L,x) . (a + b) = (Polynom-Evaluation L,x) . (p + q) by POLYNOM3:def 12
.= eval (p + q),x by Def3
.= (eval p,x) + (eval q,x) by Th22
.= ((Polynom-Evaluation L,x) . a) + (eval q,x) by Def3
.= ((Polynom-Evaluation L,x) . a) + ((Polynom-Evaluation L,x) . b) by Def3 ; :: thesis: verum