let L be non empty right_complementable Abelian add-associative right_zeroed unital distributive 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 Th22
.= (eval (p,x)) + (- (eval (q,x))) by Th23
.= (eval (p,x)) - (eval (q,x)) by RLVECT_1:def 11 ; :: thesis: verum