set f = Polynom-Evaluation (n,L,x);
for p, q being Element of (Polynom-Ring (n,L)) holds (Polynom-Evaluation (n,L,x)) . (p + q) = ((Polynom-Evaluation (n,L,x)) . p) + ((Polynom-Evaluation (n,L,x)) . q)
proof
let p,
q be
Element of
(Polynom-Ring (n,L));
(Polynom-Evaluation (n,L,x)) . (p + q) = ((Polynom-Evaluation (n,L,x)) . p) + ((Polynom-Evaluation (n,L,x)) . q)
reconsider p9 =
p,
q9 =
q as
Polynomial of
n,
L by POLYNOM1:def 11;
reconsider p =
p,
q =
q as
Element of
(Polynom-Ring (n,L)) ;
A1:
(Polynom-Evaluation (n,L,x)) . p = eval (
p9,
x)
by Def3;
(Polynom-Evaluation (n,L,x)) . (p + q) =
(Polynom-Evaluation (n,L,x)) . (p9 + q9)
by POLYNOM1:def 11
.=
eval (
(p9 + q9),
x)
by Def3
.=
(eval (p9,x)) + (eval (q9,x))
by Th15
;
hence
(Polynom-Evaluation (n,L,x)) . (p + q) = ((Polynom-Evaluation (n,L,x)) . p) + ((Polynom-Evaluation (n,L,x)) . q)
by A1, Def3;
verum
end;
hence
Polynom-Evaluation (n,L,x) is additive
by VECTSP_1:def 20; verum