let n be Ordinal; :: thesis: for L being non empty 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 empty 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 23
.= (eval p,x) + (eval (- q),x) by Th25
.= (eval p,x) + (- (eval q,x)) by Th24
.= (eval p,x) - (eval q,x) ; :: thesis: verum