let a, b be Element of (Polynom-Ring L); :: according to VECTSP_1:def 19 :: 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 10;
thus (Polynom-Evaluation (L,x)) . (a + b) = (Polynom-Evaluation (L,x)) . (p + q) by POLYNOM3:def 10
.= eval ((p + q),x) by Def3
.= (eval (p,x)) + (eval (q,x)) by Th19
.= ((Polynom-Evaluation (L,x)) . a) + (eval (q,x)) by Def3
.= ((Polynom-Evaluation (L,x)) . a) + ((Polynom-Evaluation (L,x)) . b) by Def3 ; :: thesis: verum