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