set q = (PolyHom h) . p;
h " is Isomorphism of F2,F1 by RING_3:73;
then reconsider F1i = F1 as F2 -homomorphic F2 -isomorphic Field by RING_3:def 4, RING_2:def 4;
reconsider hi = h " as Isomorphism of F2,F1i by RING_3:73;
H: (PolyHom hi) . ((PolyHom h) . p) = p

proof

now :: thesis: for i being Nat holds ((PolyHom hi) . ((PolyHom h) . p)) . i = p . i

let i be Nat; :: thesis: ((PolyHom hi) . ((PolyHom h) . p)) . i = p . i
((PolyHom h) . p) . i = h . (p . i) by FIELD_1:def 2;
hence ((PolyHom hi) . ((PolyHom h) . p)) . i = hi . (h . (p . i)) by FIELD_1:def 2
.= p . i by FUNCT_2:26 ;
:: thesis: verum

end;

hence (PolyHom hi) . ((PolyHom h) . p) = p ; :: thesis: verum

end;

now :: thesis: not (PolyHom h) . p is reducible

assume (PolyHom h) . p is reducible ; :: thesis: contradiction

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

suppose (PolyHom h) . p = 0_. F2 ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose (PolyHom h) . p is Unit of (Polynom-Ring F2) ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose ex r being Element of the carrier of (Polynom-Ring F2) st
( r divides (PolyHom h) . p & 1 <= deg r & deg r < deg ((PolyHom h) . p) ) ; :: thesis: contradiction

then consider r being Element of the carrier of (Polynom-Ring F2) such that
A: ( r divides (PolyHom h) . p & 1 <= deg r & deg r < deg ((PolyHom h) . p) ) ;
C: deg r = deg ((PolyHom hi) . r) by FIELD_1:31;
D: 1 <= deg ((PolyHom hi) . r) by A, FIELD_1:31;
deg ((PolyHom hi) . r) < deg p by A, C, FIELD_1:31;
hence contradiction by H, A, uu0, D, RING_4:40; :: thesis: verum

end;

end;

end;

hence for b₁ being Element of the carrier of (Polynom-Ring F2) st b₁ = (PolyHom h) . p holds
b₁ is irreducible ; :: thesis: verum