let L be non degenerated comRing; :: thesis: for f, g being Element of (Polynom-Ring L)
for x being Element of L holds eval ((~ (f * g)),x) = (eval ((~ f),x)) * (eval ((~ g),x))
let f, g be Element of (Polynom-Ring L); :: thesis: for x being Element of L holds eval ((~ (f * g)),x) = (eval ((~ f),x)) * (eval ((~ g),x))
let x be Element of L; :: thesis: eval ((~ (f * g)),x) = (eval ((~ f),x)) * (eval ((~ g),x))
( f is Polynomial of L & g is Polynomial of L ) by POLYNOM3:def 10;
then consider p, q being Polynomial of L such that
A1: ( p = f & q = g ) ;
A2: f * g = p *' q by A1, POLYNOM3:def 10;
( eval ((~ f),x) = eval (p,x) & eval ((~ g),x) = eval (q,x) ) by A1;
then eval ((~ (f * g)),x) = (eval ((~ f),x)) * (eval ((~ g),x)) by A2, POLYNOM4:24;
hence eval ((~ (f * g)),x) = (eval ((~ f),x)) * (eval ((~ g),x)) ; :: thesis: verum