let n be Ordinal; :: thesis: for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed commutative doubleLoopStr
for p, q being Polynomial of n,L st p - q = 0_ (n,L) holds
p = q
let L be non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed commutative doubleLoopStr ; :: thesis: for p, q being Polynomial of n,L st p - q = 0_ (n,L) holds
p = q
let p, q be Polynomial of n,L; :: thesis: ( p - q = 0_ (n,L) implies p = q )
assume p - q = 0_ (n,L) ; :: thesis: p = q
hence q = q + (p - q) by POLYNOM1:23
.= q + (p + (- q)) by POLYNOM1:def 7
.= (q + (- q)) + p by POLYNOM1:21
.= (0_ (n,L)) + p by POLYRED:3
.= p by POLYRED:2 ;
:: thesis: verum