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