let R be PIDomain; :: thesis:
let x, y be Element of R; :: thesis:
let F, G be non empty FinSequence of R; :: thesis:
assume AS: ( F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y ) ; :: thesis:
defpred S₁[ Nat] means for x, y being Element of R
for F, G being non empty FinSequence of R st len F = $1 & F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds
( len G = $1 & ex p being Function of (dom F),(dom G) st
( p is bijective & ( for i being Element of dom F holds G . (p . i) is_associated_to F . i ) ) );
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 x, y be Element of R; :: thesis:
let F, G be non empty FinSequence of R; :: thesis:
assume A3: ( len F = k + 1 & F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y ) ; :: thesis:
consider F1 being FinSequence, a being object such that
B2: F = F1 ^ <*a*> by FINSEQ_1:46;
B2a: rng F1 c= rng F by B2, FINSEQ_1:29;
rng F c= the carrier of R ;
then rng F1 c= the carrier of R by B2a;
then reconsider F1 = F1 as FinSequence of R by FINSEQ_1:def 4;
rng <*a*> = {a} by FINSEQ_1:39;
then B5: a in rng <*a*> by TARSKI:def 1;
rng <*a*> c= rng F by B2, FINSEQ_1:30;
then a in rng F by B5;
then reconsider a = a as Element of R ;
A4: len F = (len F1) + (len <*a*>) by B2, FINSEQ_1:22
.= (len F1) + 1 by FINSEQ_1:39 ;
dom <*a*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then 1 in dom <*a*> by TARSKI:def 1;
then A6: F . (k + 1) = <*a*> . 1 by B2, A4, A3, FINSEQ_1:def 7
.= a ;
dom F = Seg (k + 1) by A3, FINSEQ_1:def 3;
then A7: k + 1 in dom F by FINSEQ_1:4;
then A7a: a is irreducible by A6, A3;
A10: Product F = (Product F1) * a by B2, GROUP_4:6;
consider r being FinSequence, b being object such that
G2: G = r ^ <*b*> by FINSEQ_1:46;
G2a: rng r c= rng G by G2, FINSEQ_1:29;
rng G c= the carrier of R ;
then rng r c= the carrier of R by G2a;
then reconsider r = r as FinSequence of R by FINSEQ_1:def 4;
rng <*b*> = {b} by FINSEQ_1:39;
then G5: b in rng <*b*> by TARSKI:def 1;
rng <*b*> c= rng G by G2, FINSEQ_1:30;
then b in rng G by G5;
then reconsider b = b as Element of R ;
dom <*b*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then 1 in dom <*b*> by TARSKI:def 1;
then G6: G . ((len r) + 1) = <*b*> . 1 by G2, FINSEQ_1:def 7
.= b ;
G12: len G = (len r) + (len <*b*>) by G2, FINSEQ_1:22
.= (len r) + 1 by FINSEQ_1:39 ;
then dom G = Seg ((len r) + 1) by FINSEQ_1:def 3;
then (len r) + 1 in dom G by FINSEQ_1:4;
then G7: b is irreducible by G6, A3;
then G11: b is right_mult-cancelable by ALGSTR_0:def 37;
G9: Product G = (Product r) * b by G2, GROUP_4:6;
then G10: b divides y by A3;

per cases ;

suppose F1 = {} ; :: thesis:

then C1: F = <*a*> by B2, FINSEQ_1:34;
then C2: len F = 1 by FINSEQ_1:40;
C5: x = a by A3, C1, GROUP_4:9;
then D1: y is irreducible by A3, A7, A6, ass1;

C3: now :: thesis:

assume len G <> len F ; :: thesis:
then reconsider r = r as non empty FinSequence of R by G12, C1, FINSEQ_1:40;
consider u being Element of R such that
C4: ( u is unital & b * u = y ) by D1, G7, G10, GCD_1:18;
Product r is factorizable

proof

take r ; :: according to RING_2:def 12 :: thesis:
thus Product r = Product r ; :: according to RING_2:def 11 :: thesis:
let i be Element of dom r; :: thesis:
dom r c= dom G by G2, FINSEQ_1:26;
then reconsider j = i as Element of dom G ;
G . j is irreducible by A3;
hence r . i is irreducible by G2, FINSEQ_1:def 7; :: thesis:

end;

hence contradiction by A3, G9, C4, G11; :: thesis:

end;

then C7: G = <*(G . 1)*> by C2, FINSEQ_1:40;
then C4: ( dom G = Seg 1 & dom F = Seg 1 ) by FINSEQ_1:38, C1;
then reconsider p = id (dom F) as Function of (dom F),(dom G) ;

now :: thesis:

let i be Element of dom F; :: thesis:
E0: i = 1 by C4, TARSKI:def 1, FINSEQ_1:2;
then F . i = a by C1;
hence G . (p . i) is_associated_to F . i by E0, A3, C5, C7, GROUP_4:9; :: thesis:

end;

hence ( len G = k + 1 & ex p being Function of (dom F),(dom G) st
( p is bijective & ( for i being Element of dom F holds G . (p . i) is_associated_to F . i ) ) ) by A3, C4, C3; :: thesis:

end;

suppose F1 <> {} ; :: thesis:

then reconsider F1 = F1 as non empty FinSequence of R ;
a divides Product F by A10;
then consider j being Element of dom G such that
E1: G . j is_associated_to a by lemfactunique1, A3, A7a;
rng G c= the carrier of R ;
then reconsider g = G as Function of (dom G),R by FUNCT_2:2;
E3: g . j = g /. j ;
set G1 = Del (G,j);
consider lg1 being Nat such that
LG1: ( len G = lg1 + 1 & len (Del (G,j)) = lg1 ) by FINSEQ_3:104;
LG3: ( dom G = Seg (lg1 + 1) & dom (Del (G,j)) = Seg lg1 ) by LG1, FINSEQ_1:def 3;
then LG2: dom (Del (G,j)) c= dom G by NAT_1:11, FINSEQ_1:5;
Product G = (G . j) * (Product (Del (G,j))) by E3, RATFUNC1:3;
then a * (Product F1) is_associated_to (G . j) * (Product (Del (G,j))) by A3, B2, GROUP_4:6;
then I0: Product F1 is_associated_to Product (Del (G,j)) by A7a, E1, ass0;

now :: thesis:

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

end;

then I1: F1 is_a_factorization_of Product F1 ;

now :: thesis:

assume Del (G,j) = {} ; :: thesis:
then Del (G,j) = <*> the carrier of R ;
then Product F1 is_associated_to 1_ R by I0, GROUP_4:8;
then ( Product F1 is unital & Product F1 is factorizable ) by I1;
hence contradiction ; :: thesis:

end;

then reconsider G1 = Del (G,j) as non empty FinSequence of R ;

now :: thesis:

let i be Element of dom G1; :: thesis:
i in dom G1 ;
then i in Seg lg1 by LG1, FINSEQ_1:def 3;
then H1: ( 1 <= i & i <= lg1 ) by FINSEQ_1:1;

per cases ;

suppose G: i < j ; :: thesis:

lg1 <= lg1 + 1 by NAT_1:11;
then i <= lg1 + 1 by H1, XXREAL_0:2;
then i in Seg (lg1 + 1) by H1;
then reconsider ii = i as Element of dom G by LG1, FINSEQ_1:def 3;
G . ii is irreducible by A3;
hence G1 . i is irreducible by G, FINSEQ_3:110; :: thesis:

end;

suppose K: j <= i ; :: thesis:

( 1 <= i + 1 & i + 1 <= lg1 + 1 ) by H1, XREAL_1:6, NAT_1:11;
then i + 1 in Seg (lg1 + 1) ;
then reconsider ii = i + 1 as Element of dom G by LG1, FINSEQ_1:def 3;
G . ii is irreducible by A3;
hence G1 . i is irreducible by K, H1, LG1, FINSEQ_3:111; :: thesis:

end;

then I2: G1 is_a_factorization_of Product G1 ;
II: ( len G1 = k & ex p being Function of (dom F1),(dom G1) st
( p is bijective & ( for i being Element of dom F1 holds G1 . (p . i) is_associated_to F1 . i ) ) ) by IV, A4, A3, I0, I1, I2;
thus III: len G = k + 1 by IV, A4, A3, I0, I1, I2, LG1; :: thesis:
consider p being Function of (dom F1),(dom G1) such that
P0: ( p is bijective & ( for i being Element of dom F1 holds G1 . (p . i) is_associated_to F1 . i ) ) by IV, A4, A3, I0, I1, I2;
R0: ( p is one-to-one & p is onto ) by P0;
R1: rng p = dom G1 by P0, FUNCT_2:def 3;
defpred S₂[ Nat, Nat] means ( ( $2 = p . $1 & p . $1 < j & $1 <> k + 1 ) or ( $2 = (p . $1) + 1 & p . $1 >= j & $1 <> k + 1 ) or ( $2 = j & $1 = k + 1 ) );
P1: for x being Element of dom F ex y being Element of dom G st S₂[x,y]

proof

let x be Element of dom F; :: thesis:
dom F = Seg (k + 1) by A3, FINSEQ_1:def 3;
then Q0: ( 1 <= x & x <= k + 1 ) by FINSEQ_1:1;

per cases ;

suppose Q1: x = k + 1 ; :: thesis:

take j ; :: thesis:
thus S₂[x,j] by Q1; :: thesis:

end;

suppose Q1: x <> k + 1 ; :: thesis:

then x < k + 1 by Q0, XXREAL_0:1;
then x <= k by NAT_1:13;
then Q2: x in Seg k by Q0;
dom F1 = Seg k by A3, A4, FINSEQ_1:def 3;
then Q: p . x in dom G1 by Q2, R1, FUNCT_2:4;
then ( 1 <= p . x & p . x <= k ) by III, LG1, LG3, FINSEQ_1:1;
then ( 1 <= (p . x) + 1 & (p . x) + 1 <= k + 1 ) by NAT_1:11, XREAL_1:6;
then R: (p . x) + 1 in Seg (k + 1) ;

now :: thesis:

per cases ;

suppose Q3: p . x < j ; :: thesis:

reconsider px = p . x as Element of dom G by Q, LG2;
take px = px; :: thesis:
( px = p . x & p . x < j & x <> k + 1 ) by Q1, Q3;
hence ex y being Element of dom G st S₂[x,y] ; :: thesis:

end;

suppose Q3: p . x >= j ; :: thesis:

reconsider px1 = (p . x) + 1 as Element of dom G by III, R, FINSEQ_1:def 3;
take px1 = px1; :: thesis:
( px1 = (p . x) + 1 & p . x >= j & x <> k + 1 ) by Q1, Q3;
hence ex y being Element of dom G st S₂[x,y] ; :: thesis:

end;

hence ex y being Element of dom G st S₂[x,y] ; :: thesis:

end;

consider B being Function of (dom F),(dom G) such that
P2: for x being Element of dom F holds S₂[x,B . x] from FUNCT_2:sch 3(P1);
take B = B; :: thesis:

now :: thesis:

let x1, x2 be object ; :: thesis:
assume S0: ( x1 in dom F & x2 in dom F & B . x1 = B . x2 ) ; :: thesis:
then reconsider x = x1, y = x2 as Element of dom F ;
S1: dom F = Seg (k + 1) by A3, FINSEQ_1:def 3;
then S2: ( 1 <= x & x <= k + 1 ) by FINSEQ_1:1;
S3: ( 1 <= y & y <= k + 1 ) by S1, FINSEQ_1:1;

per cases ;

suppose S4: x = k + 1 ; :: thesis:

then S5: j = B . y by S0, P2;

now :: thesis:

assume S6: y <> k + 1 ; :: thesis:

per cases ;

suppose p . y < j ; :: thesis:

hence contradiction by S5, S6, P2; :: thesis:

end;

suppose S7: p . y >= j ; :: thesis:

then S9: (p . y) + 1 = B . y by S6, P2
.= j by S4, S0, P2 ;
consider k being Nat such that
S8: p . y = j + k by S7, NAT_1:10;
p . y = j - 1 by S9;
hence contradiction by S8; :: thesis:

end;

hence x1 = x2 by S4; :: thesis:

end;