let F be Field; for p being irreducible Element of the carrier of (Polynom-Ring F)
for a, b being Element of the carrier of (Polynom-Ring F)
for q, r being Element of (Polynom-Ring p) st a = q & b = r holds
a - b = q - r
let p be irreducible Element of the carrier of (Polynom-Ring F); for a, b being Element of the carrier of (Polynom-Ring F)
for q, r being Element of (Polynom-Ring p) st a = q & b = r holds
a - b = q - r
let a, b be Element of the carrier of (Polynom-Ring F); for q, r being Element of (Polynom-Ring p) st a = q & b = r holds
a - b = q - r
let q, r be Element of (Polynom-Ring p); ( a = q & b = r implies a - b = q - r )
assume A1:
( a = q & b = r )
; a - b = q - r
then
- b = - r
by Lm9;
then A2:
[a,(- b)] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):]
by A1, ZFMISC_1:def 2;
A3:
the addF of (Polynom-Ring p) = the addF of (Polynom-Ring F) || the carrier of (Polynom-Ring p)
by RING_4:def 8;
a - b =
the addF of (Polynom-Ring p) . (a,(- b))
by A2, A3, FUNCT_1:49
.=
q - r
by A1, Lm9
;
hence
a - b = q - r
; verum