let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q being Polynomial of L st p - q = 0_. L holds

p = q

let q, r be Polynomial of L; :: thesis: ( q - r = 0_. L implies q = r )

set PRL = Polynom-Ring L;

reconsider qc = q, rc = r as Element of (Polynom-Ring L) by POLYNOM3:def 10;

assume A1: q - r = 0_. L ; :: thesis: q = r

0_. L = 0. (Polynom-Ring L) by POLYNOM3:def 10;

then qc - rc = 0. (Polynom-Ring L) by A1, Th22;

hence q = r by VECTSP_1:27; :: thesis: verum

p = q

let q, r be Polynomial of L; :: thesis: ( q - r = 0_. L implies q = r )

set PRL = Polynom-Ring L;

reconsider qc = q, rc = r as Element of (Polynom-Ring L) by POLYNOM3:def 10;

assume A1: q - r = 0_. L ; :: thesis: q = r

0_. L = 0. (Polynom-Ring L) by POLYNOM3:def 10;

then qc - rc = 0. (Polynom-Ring L) by A1, Th22;

hence q = r by VECTSP_1:27; :: thesis: verum