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

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