let n be Ordinal; :: thesis: for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive 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 associative commutative well-unital distributive 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:27
.= a * (eval p,x) by Th25 ; :: thesis: verum