let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 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 ; :: thesis: verum

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 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 ; :: thesis: verum