let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Element of (Polynom-Ring (n,L))
for x being Function of n,L holds E_eval ((f * g),x) = (E_eval (f,x)) * (E_eval (g,x))
let L be non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, g being Element of (Polynom-Ring (n,L))
for x being Function of n,L holds E_eval ((f * g),x) = (E_eval (f,x)) * (E_eval (g,x))
let f, g be Element of (Polynom-Ring (n,L)); :: thesis: for x being Function of n,L holds E_eval ((f * g),x) = (E_eval (f,x)) * (E_eval (g,x))
let x be Function of n,L; :: thesis: E_eval ((f * g),x) = (E_eval (f,x)) * (E_eval (g,x))
( f in [#] (Polynom-Ring (n,L)) & g in [#] (Polynom-Ring (n,L)) ) by SUBSET_1:def 1;
then ( f is Polynomial of n,L & g is Polynomial of n,L ) by POLYNOM1:def 11;
then consider p, q being Polynomial of n,L such that
A1: ( p = f & q = g ) ;
A2: f * g = p *' q by A1, POLYNOM1:def 11;
A3: ( E_eval (f,x) = eval (p,x) & E_eval (g,x) = eval (q,x) ) by A1, Def1;
E_eval ((f * g),x) = eval ((p *' q),x) by A2, Def1
.= (E_eval (f,x)) * (E_eval (g,x)) by A3, POLYNOM2:25 ;
hence E_eval ((f * g),x) = (E_eval (f,x)) * (E_eval (g,x)) ; :: thesis: verum