let F be Field; :: thesis: for E being FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st q = p & q is irreducible holds
p is irreducible
let E be FieldExtension of F; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st q = p & q is irreducible holds
p is irreducible
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for q being Element of the carrier of (Polynom-Ring E) st q = p & q is irreducible holds
p is irreducible
let q be Element of the carrier of (Polynom-Ring E); :: thesis: ( q = p & q is irreducible implies p is irreducible )
assume AS1: q = p ; :: thesis: ( not q is irreducible or p is irreducible )
assume AS: q is irreducible ; :: thesis: p is irreducible

now :: thesis: ( p is reducible implies q is reducible )

assume p is reducible ; :: thesis: q is reducible

per cases then ( p = 0_. F or p is Unit of (Polynom-Ring F) or ex p1 being Element of the carrier of (Polynom-Ring F) st
( p1 divides p & 1 <= deg p1 & deg p1 < deg p ) ) by RING_4:41;

suppose p = 0_. F ; :: thesis: q is reducible

then q = 0_. E by AS1, FIELD_4:12;
hence q is reducible ; :: thesis: verum

end;

suppose p is Unit of (Polynom-Ring F) ; :: thesis: q is reducible

then deg p = 0 by RING_4:37;
then deg q = 0 by AS1, FIELD_4:20;
hence q is reducible by RING_4:37; :: thesis: verum

end;

suppose ex p1 being Element of the carrier of (Polynom-Ring F) st
( p1 divides p & 1 <= deg p1 & deg p1 < deg p ) ; :: thesis: q is reducible

then consider p1 being Element of the carrier of (Polynom-Ring F) such that
A: ( p1 divides p & 1 <= deg p1 & deg p1 < deg p ) ;
consider r being Polynomial of F such that
B: p1 *' r = p by A, RING_4:1;
( p1 is Polynomial of E & r is Polynomial of E ) by FIELD_4:8;
then reconsider q1 = p1, s = r as Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
( q1 *' s = q & deg q1 = deg p1 & deg q = deg p ) by B, AS1, FIELD_4:17, FIELD_4:20;
hence q is reducible by A, RING_4:1, RING_4:41; :: thesis: verum

end;

end;

end;

hence p is irreducible by AS; :: thesis: verum