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

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