set R = INT.Ring ;
set K = Polynom-Ring INT.Ring;
set a = (1. INT.Ring) + (1. INT.Ring);
set p = (((1. INT.Ring) + (1. INT.Ring)) | INT.Ring) *' (rpoly (1,(0. INT.Ring)));
(1. INT.Ring) + (1. INT.Ring) <> 0. INT.Ring ;
then reconsider a = (1. INT.Ring) + (1. INT.Ring) as non zero Element of INT.Ring by STRUCT_0:def 12;
reconsider q = a | INT.Ring as Element of the carrier of (Polynom-Ring INT.Ring) by POLYNOM3:def 10;
q is constant by RATFUNC1:def 2;
then reconsider q = q as non zero constant Element of the carrier of (Polynom-Ring INT.Ring) ;
reconsider r = rpoly (1,(0. INT.Ring)) as Element of the carrier of (Polynom-Ring INT.Ring) by POLYNOM3:def 10;
A1: (((1. INT.Ring) + (1. INT.Ring)) | INT.Ring) *' (rpoly (1,(0. INT.Ring))) = (a * (1_. INT.Ring)) *' (rpoly (1,(0. INT.Ring))) by LX1
.= a * ((1_. INT.Ring) *' (rpoly (1,(0. INT.Ring)))) by poly2
.= a * (rpoly (1,(0. INT.Ring))) by poly1 ;
A2: deg ((((1. INT.Ring) + (1. INT.Ring)) | INT.Ring) *' (rpoly (1,(0. INT.Ring)))) = (deg q) + (deg (rpoly (1,(0. INT.Ring)))) by HURWITZ:23
.= 0 + (deg (rpoly (1,(0. INT.Ring)))) by LX
.= 1 by HURWITZ:27 ;
then ((((1. INT.Ring) + (1. INT.Ring)) | INT.Ring) *' (rpoly (1,(0. INT.Ring)))) . ((len ((((1. INT.Ring) + (1. INT.Ring)) | INT.Ring) *' (rpoly (1,(0. INT.Ring))))) -' 1) = (a * (rpoly (1,(0. INT.Ring)))) . (2 - 1) by A1, XREAL_1:233
.= a * ((rpoly (1,(0. INT.Ring))) . 1) by POLYNOM5:def 4
.= a * (1. INT.Ring) by HURWITZ:25
.= a ;
then LC ((((1. INT.Ring) + (1. INT.Ring)) | INT.Ring) *' (rpoly (1,(0. INT.Ring)))) = a ;
then reconsider pp = (((1. INT.Ring) + (1. INT.Ring)) | INT.Ring) *' (rpoly (1,(0. INT.Ring))) as non monic Element of the carrier of (Polynom-Ring INT.Ring) by RATFUNC1:def 7, POLYNOM3:def 10;
take pp ; :: thesis: ( deg pp = 1 & pp is reducible )
thus deg pp = 1 by A2; :: thesis: pp is reducible
B0: (((1. INT.Ring) + (1. INT.Ring)) | INT.Ring) *' (rpoly (1,(0. INT.Ring))) = q * r by POLYNOM3:def 10;
B1: q divides pp by B0, GCD_1:def 1;
B4: now :: thesis: q is not Unit of (Polynom-Ring INT.Ring)
assume q is Unit of (Polynom-Ring INT.Ring) ; :: thesis: contradiction
then a is Unit of INT.Ring by Th90;
then a divides 1. INT.Ring by GCD_1:def 2;
then consider c being Element of the carrier of INT.Ring such that
C1: a * c = 1. INT.Ring ;
thus contradiction by C1, INT_1:9; :: thesis: verum
end;
now :: thesis: not q is_associated_to pp
assume q is_associated_to pp ; :: thesis: contradiction
then consider c being Element of the carrier of (Polynom-Ring INT.Ring) such that
C1: ( c is unital & q * c = (((1. INT.Ring) + (1. INT.Ring)) | INT.Ring) *' (rpoly (1,(0. INT.Ring))) ) by GCD_1:18;
C2: (a | INT.Ring) *' c = (((1. INT.Ring) + (1. INT.Ring)) | INT.Ring) *' (rpoly (1,(0. INT.Ring))) by C1, POLYNOM3:def 10;
deg c = 0 by C1, T88;
then c <> 0_. INT.Ring by HURWITZ:20;
then 1 = (deg q) + (deg c) by HURWITZ:23, C2, A2
.= 0 + (deg c) by LX ;
hence contradiction by C1, T88; :: thesis: verum
end;
hence pp is reducible by B1, B4, RING_2:def 9; :: thesis: verum