let n be Ordinal; :: thesis: for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for x being Function of n,L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x))
let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p, q being Polynomial of n,L
for x being Function of n,L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x))
let p, q be Polynomial of n,L; :: thesis: for x being Function of n,L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x))
let x be Function of n,L; :: thesis: eval ((p - q),x) = (eval (p,x)) - (eval (q,x))
thus eval ((p - q),x) = eval ((p + (- q)),x) by POLYNOM1:def 7
.= (eval (p,x)) + (eval ((- q),x)) by Th15
.= (eval (p,x)) - (eval (q,x)) by Th14 ; :: thesis: verum