let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L
for f, g being Element of (Polynom-Ring n,L) st f = p & g = q holds
f - g = p - q
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L
for f, g being Element of (Polynom-Ring n,L) st f = p & g = q holds
f - g = p - q
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q being Polynomial of n,L
for f, g being Element of (Polynom-Ring n,L) st f = p & g = q holds
f - g = p - q
let p, q be Polynomial of n,L; :: thesis: for f, g being Element of (Polynom-Ring n,L) st f = p & g = q holds
f - g = p - q
let f, g be Element of (Polynom-Ring n,L); :: thesis: ( f = p & g = q implies f - g = p - q )
assume that
A1: f = p and
A2: g = q ; :: thesis: f - g = p - q
reconsider x = - q as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider x = x as Element of (Polynom-Ring n,L) ;
x + g = (- q) + q by A2, POLYNOM1:def 27
.= 0_ n,L by POLYRED:3
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;
then A3: - q = - g by RLVECT_1:19;
thus p - q = p + (- q) by POLYNOM1:def 23
.= f + (- g) by A1, A3, POLYNOM1:def 27
.= f - g by RLVECT_1:def 14 ; :: thesis: verum