let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q being Polynomial of L
for pc, qc being Element of (Polynom-Ring L) st p = pc & q = qc holds
p - q = pc - qc
let p, q be Polynomial of L; :: thesis: for pc, qc being Element of (Polynom-Ring L) st p = pc & q = qc holds
p - q = pc - qc
let pc, qc be Element of (Polynom-Ring L); :: thesis: ( p = pc & q = qc implies p - q = pc - qc )
assume that
A1: p = pc and
A2: q = qc ; :: thesis: p - q = pc - qc
- q = - qc by A2, Th21;
hence p - q = pc - qc by A1, POLYNOM3:def 10; :: thesis: verum