let L be non empty right_complementable Abelian add-associative right_zeroed distributive unital doubleLoopStr ; :: thesis: for p, q being Polynomial of L
for x being Element of L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x))
let p, q be Polynomial of L; :: thesis: for x being Element of L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x))
let x be Element of L; :: thesis: eval ((p - q),x) = (eval (p,x)) - (eval (q,x))
thus eval ((p - q),x) = (eval (p,x)) + (eval ((- q),x)) by Th19
.= (eval (p,x)) + (- (eval (q,x))) by Th20
.= (eval (p,x)) - (eval (q,x)) by RLVECT_1:def 11 ; :: thesis: verum