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 ((p *' (a | (n,L))),x) = (eval (p,x)) * a
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 ((p *' (a | (n,L))),x) = (eval (p,x)) * a
let p be Polynomial of n,L; :: thesis: for a being Element of L
for x being Function of n,L holds eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
let a be Element of L; :: thesis: for x being Function of n,L holds eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
let x be Function of n,L; :: thesis: eval ((p *' (a | (n,L))),x) = (eval (p,x)) * a
thus eval ((p *' (a | (n,L))),x) = (eval (p,x)) * (eval ((a | (n,L)),x)) by POLYNOM2:25
.= (eval (p,x)) * a by Th25 ; :: thesis: verum