let R be domRing; :: thesis:
let a, b, x be Element of R; :: thesis:
let F be non empty FinSequence of R; :: thesis:
assume AS: ( x is prime & x divides a & a is_associated_to b & F is_a_factorization_of b ) ; :: thesis:
defpred S₁[ Nat] means for F being non empty FinSequence of R
for a, b being Element of R st len F = $1 & x divides a & a is_associated_to b & F is_a_factorization_of b holds
ex i being Element of dom F st F . i is_associated_to x;
A0: S₁[ 0 ] ;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume IV: S₁[k] ; :: thesis:

now :: thesis:

let F be non empty FinSequence of R; :: thesis:
let a, b be Element of R; :: thesis:
assume A3: ( len F = k + 1 & x divides a & a is_associated_to b & F is_a_factorization_of b ) ; :: thesis:
consider q being FinSequence, y being object such that
B2: F = q ^ <*y*> by FINSEQ_1:46;
B2a: rng q c= rng F by B2, FINSEQ_1:29;
rng F c= the carrier of R ;
then rng q c= the carrier of R by B2a;
then reconsider q = q as FinSequence of R by FINSEQ_1:def 4;
rng <*y*> = {y} by FINSEQ_1:39;
then B5: y in rng <*y*> by TARSKI:def 1;
rng <*y*> c= rng F by B2, FINSEQ_1:30;
then y in rng F by B5;
then reconsider y = y as Element of R ;
A4: len F = (len q) + (len <*y*>) by B2, FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:39 ;
A5: b = (Product q) * y by GROUP_4:6, B2, A3;
dom <*y*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then 1 in dom <*y*> by TARSKI:def 1;
then A6: F . (k + 1) = <*y*> . 1 by B2, A4, A3, FINSEQ_1:def 7
.= y by FINSEQ_1:def 8 ;
dom F = Seg (k + 1) by A3, FINSEQ_1:def 3;
then A8: k + 1 in dom F by FINSEQ_1:4;
then A7: y is irreducible by A6, A3;
consider d being Element of R such that
Z: ( d is unital & a * d = b ) by A3, GCD_1:18;
A9: x divides b by Z, A3, GCD_1:7;

per cases by A5, A9, AS;

suppose x divides y ; :: thesis:

then x is_associated_to y by AS, A7;
hence ex i being Element of dom F st F . i is_associated_to x by A8, A6; :: thesis:

end;

suppose C0: x divides Product q ; :: thesis:

now :: thesis:

per cases ;

suppose q = {} ; :: thesis:

then b = Product <*y*> by A3, B2, FINSEQ_1:34
.= y by GROUP_4:9 ;
then x is_associated_to y by AS, A7, Z, A3, GCD_1:7;
hence ex i being Element of dom F st F . i is_associated_to x by A6, A8; :: thesis:

end;

suppose q <> {} ; :: thesis:

then reconsider q = q as non empty FinSequence of R ;

now :: thesis:

let i be Element of dom q; :: thesis:
dom q c= dom F by B2, FINSEQ_1:26;
then reconsider j = i as Element of dom F ;
F . j is irreducible by A3;
hence q . i is irreducible by B2, FINSEQ_1:def 7; :: thesis:

end;

then q is_a_factorization_of Product q ;
then consider i being Element of dom q such that
C1: q . i is_associated_to x by IV, C0, A3, A4;
C3: F . i = q . i by B2, FINSEQ_1:def 7;
dom q c= dom F by B2, FINSEQ_1:26;
then i in dom F ;
hence ex i being Element of dom F st F . i is_associated_to x by C1, C3; :: thesis:

end;

end;

end;

hence ex i being Element of dom F st F . i is_associated_to x ; :: thesis:

end;

end;

end;

hence S₁[k + 1] ; :: thesis:

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(A0, A1);
ex n being Nat st len F = n ;
hence ex i being Element of dom F st F . i is_associated_to x by I, AS; :: thesis: