let n be Ordinal; 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; 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 ; 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; 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)); ( f = p & g = q implies f - g = p - q )
assume that
A1:
f = p
and
A2:
g = q
; f - g = p - q
reconsider x = - q as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider x = x as Element of (Polynom-Ring (n,L)) ;
x + g =
(- q) + q
by A2, POLYNOM1:def 11
.=
0_ (n,L)
by POLYRED:3
.=
0. (Polynom-Ring (n,L))
by POLYNOM1:def 11
;
then A3:
- q = - g
by RLVECT_1:6;
thus p - q =
p + (- q)
by POLYNOM1:def 7
.=
f + (- g)
by A1, A3, POLYNOM1:def 11
.=
f - g
; verum