let R be comRing; :: thesis: for p being Polynomial of R
for a being Element of R holds eval ((<%(0. R),(1. R)%> *' p),a) = a * (eval (p,a))
let p be Polynomial of R; :: thesis: for a being Element of R holds eval ((<%(0. R),(1. R)%> *' p),a) = a * (eval (p,a))
let a be Element of R; :: thesis: eval ((<%(0. R),(1. R)%> *' p),a) = a * (eval (p,a))

per cases ( R is degenerated or not R is degenerated ) ;

suppose R is degenerated ; :: thesis: eval ((<%(0. R),(1. R)%> *' p),a) = a * (eval (p,a))

then A: the carrier of R = {(0. R)} by degen;
hence eval ((<%(0. R),(1. R)%> *' p),a) = 0. R by TARSKI:def 1
.= a * (eval (p,a)) by A, TARSKI:def 1 ;
:: thesis: verum

end;

suppose not R is degenerated ; :: thesis: eval ((<%(0. R),(1. R)%> *' p),a) = a * (eval (p,a))

hence eval ((<%(0. R),(1. R)%> *' p),a) = (eval (<%(0. R),(1. R)%>,a)) * (eval (p,a)) by POLYNOM4:24
.= ((0. R) + ((1. R) * a)) * (eval (p,a)) by POLYNOM5:44
.= a * (eval (p,a)) ;
:: thesis: verum

end;

end;