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 14 ; :: thesis: verum