let R be domRing; :: thesis: ( R is PID implies R is factorial )
assume Z: R is PID ; :: thesis: R is factorial
assume not R is factorial ; :: thesis: contradiction
then consider a0 being non zero Element of R such that
XX: ( a0 is NonUnit of R & not a0 is uniquely_factorizable ) ;

now :: thesis: a0 is factorizable

assume X: not a0 is factorizable ; :: thesis: contradiction
{a0} -Ideal in Ideals R ;
then reconsider A = {a0} -Ideal as Element of Ideals R ;
defpred S₁[ set , set , set ] means for a being Element of R st a <> 0. R & not a is unital & not a is factorizable & c₂ = {a} -Ideal holds
ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & c₃ = {a1} -Ideal & {a} -Ideal c= {a1} -Ideal & {a} -Ideal <> {a1} -Ideal );
A: for n being Nat
for x being Element of Ideals R ex y being Element of Ideals R st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Element of Ideals R ex y being Element of Ideals R st S₁[n,x,y]
let x be Element of Ideals R; :: thesis: ex y being Element of Ideals R st S₁[n,x,y]
A1: for a being Element of R st a <> 0. R & not a is unital & not a is factorizable & x = {a} -Ideal holds
ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & x c= {a1} -Ideal & x <> {a1} -Ideal )

proof

let a be Element of R; :: thesis: ( a <> 0. R & not a is unital & not a is factorizable & x = {a} -Ideal implies ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & x c= {a1} -Ideal & x <> {a1} -Ideal ) )
assume A1: ( a <> 0. R & not a is unital & not a is factorizable & x = {a} -Ideal ) ; :: thesis: ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & x c= {a1} -Ideal & x <> {a1} -Ideal )
then a is reducible ;
then consider u being Element of R such that
A3: ( u divides a & not u is unital & not u is_associated_to a ) by A1;
consider s being Element of R such that
A4: u * s = a by A3;

A5: now :: thesis: ( u is factorizable implies not s is factorizable )

assume ( u is factorizable & s is factorizable ) ; :: thesis: contradiction
then consider F, G being non empty FinSequence of R such that
H: ( F is_a_factorization_of u & G is_a_factorization_of s ) ;
F ^ G is_a_factorization_of a by A4, H, fact2;
hence contradiction by A1; :: thesis: verum

end;

now :: thesis: ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & x c= {a1} -Ideal & x <> {a1} -Ideal )

per cases ( not s is factorizable or not u is factorizable ) by A5;

suppose B1: not s is factorizable ; :: thesis: ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & x c= {a1} -Ideal & x <> {a1} -Ideal )

B2: s divides a by A4;
B4: s <> 0. R by A1, A4;
then H: s is right_mult-cancelable by ALGSTR_0:def 37;

B3: now :: thesis: not {a} -Ideal = {s} -Ideal

assume {a} -Ideal = {s} -Ideal ; :: thesis: contradiction
then ex e being Element of R st
( e is unital & s * e = a ) by GCD_1:18, div3;
hence contradiction by H, A4, A3; :: thesis: verum

end;

not s is unital by A4, A3, GCD_1:18;
hence ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & x c= {a1} -Ideal & x <> {a1} -Ideal ) by B1, B2, B3, B4, A1, div1; :: thesis: verum

end;

suppose B1: not u is factorizable ; :: thesis: ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & x c= {a1} -Ideal & x <> {a1} -Ideal )

B3: {a} -Ideal <> {u} -Ideal by A3, div1;
u <> 0. R by A4, A1;
hence ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & x c= {a1} -Ideal & x <> {a1} -Ideal ) by B1, A3, div1, B3, A1; :: thesis: verum

end;

end;

end;

hence ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & x c= {a1} -Ideal & x <> {a1} -Ideal ) ; :: thesis: verum

end;

now :: thesis: ex Y being Element of Ideals R st S₁[n,x,Y]

per cases ( ex a being Element of R st
( a <> 0. R & not a is unital & not a is factorizable & x = {a} -Ideal ) or for a being Element of R holds
( not a <> 0. R or a is unital or a is factorizable or not x = {a} -Ideal ) ) ;

suppose AA: ex a being Element of R st
( a <> 0. R & not a is unital & not a is factorizable & x = {a} -Ideal ) ; :: thesis: ex Y being Element of Ideals R st S₁[n,x,Y]

consider a1 being Element of R such that
A3: ( a1 <> 0. R & not a1 is unital & not a1 is factorizable & x c= {a1} -Ideal & x <> {a1} -Ideal ) by A1, AA;
{a1} -Ideal in Ideals R ;
then reconsider A1 = {a1} -Ideal as Element of Ideals R ;
S₁[n,x,A1] by A3;
hence ex Y being Element of Ideals R st S₁[n,x,Y] ; :: thesis: verum

end;

suppose AA: for a being Element of R holds
( not a <> 0. R or a is unital or a is factorizable or not x = {a} -Ideal ) ; :: thesis: ex y being Element of Ideals R st S₁[n,x,y]

A1: {(0. R)} in Ideals R ;
S₁[n,x,{(0. R)}] by AA;
hence ex y being Element of Ideals R st S₁[n,x,y] by A1; :: thesis: verum

end;

end;

end;

hence ex y being Element of Ideals R st S₁[n,x,y] ; :: thesis: verum

end;

ex f being sequence of (Ideals R) st
( f . 0 = A & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A);
then consider F being sequence of (Ideals R) such that
C1: ( F . 0 = A & ( for n being Nat holds S₁[n,F . n,F . (n + 1)] ) ) ;
B: for i being Nat holds
( F . i c= F . (i + 1) & F . i <> F . (i + 1) )

proof

let i be Nat; :: thesis: ( F . i c= F . (i + 1) & F . i <> F . (i + 1) )
defpred S₂[ Nat] means ( ex a being Element of R st
( a <> 0. R & not a is unital & not a is factorizable & F . (c₁ + 1) = {a} -Ideal ) & F . c₁ c= F . (c₁ + 1) & F . c₁ <> F . (c₁ + 1) );
A: S₂[ 0 ]

proof

A0: S₁[ 0 ,F . 0,F . (0 + 1)] by C1;
A3: ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & F . 1 = {a1} -Ideal & {a0} -Ideal c= {a1} -Ideal & {a0} -Ideal <> {a1} -Ideal ) by A0, C1, X, XX;
thus ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & F . (0 + 1) = {a1} -Ideal ) by A3; :: thesis: ( F . 0 c= F . (0 + 1) & F . 0 <> F . (0 + 1) )
thus ( F . 0 c= F . (0 + 1) & F . 0 <> F . (0 + 1) ) by A3, C1; :: thesis: verum

end;

B: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[k + 1]
then consider a being Element of R such that
B1: ( a <> 0. R & not a is unital & not a is factorizable & F . (k + 1) = {a} -Ideal & F . k c= F . (k + 1) & F . k <> F . (k + 1) ) ;
ex a1 being Element of R st
( a1 <> 0. R & not a1 is unital & not a1 is factorizable & F . ((k + 1) + 1) = {a1} -Ideal & {a} -Ideal c= {a1} -Ideal & {a} -Ideal <> {a1} -Ideal ) by B1, C1;
hence S₂[k + 1] by B1; :: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A, B);
hence ( F . i c= F . (i + 1) & F . i <> F . (i + 1) ) ; :: thesis: verum

end;

then reconsider F = F as ascending Chain of (Ideals R) by asc;

now :: thesis: not F is stagnating

assume F is stagnating ; :: thesis: contradiction
then consider i being Nat such that
D1: for j being Nat st j >= i holds
F . j = F . i ;
F . (i + 1) = F . i by D1, NAT_1:11;
hence contradiction by B; :: thesis: verum

end;

hence contradiction by Z; :: thesis: verum

end;

hence contradiction by Z, XX; :: thesis: verum