let n be Ordinal; :: thesis: for L being non trivial right_complementable commutative well-unital distributive Abelian add-associative right_zeroed 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 commutative well-unital distributive Abelian add-associative right_zeroed 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:82
.= q + (p + (- q)) by POLYNOM1:def 23
.= (q + (- q)) + p by POLYNOM1:80
.= (0_ n,L) + p by POLYRED:3
.= p by POLYRED:2 ;
:: thesis: verum