let F be Field; :: thesis: 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); :: thesis: 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); :: thesis: 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); :: thesis: ( a = q & b = r implies a - b = q - r )
assume A1: ( a = q & b = r ) ; :: thesis: 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 ; :: thesis: verum