let n be Ordinal; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: verum

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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: verum