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;