let n be Ordinal; for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr ; for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
let p be Polynomial of n,L; for a being Element of L
for x being Function of n,L holds eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
let a be Element of L; for x being Function of n,L holds eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
let x be Function of n,L; eval (((a | (n,L)) *' p),x) = a * (eval (p,x))
thus eval (((a | (n,L)) *' p),x) =
(eval ((a | (n,L)),x)) * (eval (p,x))
by POLYNOM2:25
.=
a * (eval (p,x))
by Th25
; verum