let R be PIDomain; for x, y being Element of R
for F, G being non empty FinSequence of R st F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds
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 ) )
let x, y be Element of R; for F, G being non empty FinSequence of R st F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds
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 ) )
let F, G be non empty FinSequence of R; ( F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y implies 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 ) ) )
assume AS:
( F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y )
; 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 ) )
defpred S1[ 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:
S1[ 0 ]
;
A1:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume IV:
S1[
k]
;
S1[k + 1]
now for x, y being Element of R
for F, G being non empty FinSequence of R st len F = k + 1 & F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds
( 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 ) ) )let x,
y be
Element of
R;
for F, G being non empty FinSequence of R st len F = k + 1 & F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds
( len b6 = k + 1 & ex p being Function of (dom b5),(dom b6) st
( b7 is bijective & ( for i being Element of dom b5 holds b6 . (b7 . b8) is_associated_to b5 . b8 ) ) )let F,
G be non
empty FinSequence of
R;
( len F = k + 1 & F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y implies ( len b4 = k + 1 & ex p being Function of (dom b3),(dom b4) st
( b5 is bijective & ( for i being Element of dom b3 holds b4 . (b5 . b6) is_associated_to b3 . b6 ) ) ) )assume A3:
(
len F = k + 1 &
F is_a_factorization_of x &
G is_a_factorization_of y &
x is_associated_to y )
;
( len b4 = k + 1 & ex p being Function of (dom b3),(dom b4) st
( b5 is bijective & ( for i being Element of dom b3 holds b4 . (b5 . b6) is_associated_to b3 . b6 ) ) )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
by FINSEQ_1:def 8
;
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
by FINSEQ_1:def 8
;
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
( F1 = {} or F1 <> {} )
;
suppose
F1 = {}
;
( len b4 = k + 1 & ex p being Function of (dom b3),(dom b4) st
( b5 is bijective & ( for i being Element of dom b3 holds b4 . (b5 . b6) is_associated_to b3 . b6 ) ) )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;
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) ;
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;
verum end; suppose
F1 <> {}
;
( len b4 = k + 1 & ex B being Function of (dom b3),(dom b4) st
( b5 is bijective & ( for i being Element of dom b3 holds b4 . (b5 . b6) is_associated_to b3 . b6 ) ) )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;
then I1:
F1 is_a_factorization_of Product F1
;
then reconsider G1 =
Del (
G,
j) as non
empty FinSequence of
R ;
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;
ex B being Function of (dom F),(dom G) st
( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) )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 S2[
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
S2[
x,
y]
proof
let x be
Element of
dom F;
ex y being Element of dom G st S2[x,y]
dom F = Seg (k + 1)
by A3, FINSEQ_1:def 3;
then Q0:
( 1
<= x &
x <= k + 1 )
by FINSEQ_1:1;
per cases
( x = k + 1 or x <> k + 1 )
;
suppose Q1:
x = k + 1
;
ex y being Element of dom G st S2[x,y]take
j
;
S2[x,j]thus
S2[
x,
j]
by Q1;
verum end; suppose Q1:
x <> k + 1
;
ex y being Element of dom G st S2[x,y]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)
;
hence
ex
y being
Element of
dom G st
S2[
x,
y]
;
verum end;
end; consider B being
Function of
(dom F),
(dom G) such that P2:
for
x being
Element of
dom F holds
S2[
x,
B . x]
from FUNCT_2:sch 3(P1);
take B =
B;
( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) )now for x1, x2 being object st x1 in dom F & x2 in dom F & B . x1 = B . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in dom F & x2 in dom F & B . x1 = B . x2 implies b1 = b2 )assume S0:
(
x1 in dom F &
x2 in dom F &
B . x1 = B . x2 )
;
b1 = b2then 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
( x = k + 1 or x <> k + 1 )
;
suppose S4:
x = k + 1
;
b1 = b2then S5:
j = B . y
by S0, P2;
now not y <> k + 1assume S6:
y <> k + 1
;
contradiction end; hence
x1 = x2
by S4;
verum end; suppose Q1:
x <> k + 1
;
b1 = b2then
x < k + 1
by S2, XXREAL_0:1;
then
x <= k
by NAT_1:13;
then Q2:
x in Seg k
by S2;
Q4:
x in dom F1
by Q2, A3, A4, FINSEQ_1:def 3;
Q8:
now not y = k + 1assume R0:
y = k + 1
;
contradictionthen R1:
j = B . x
by P2, S0;
B . x <> j
hence
contradiction
by R0, S0, P2;
verum end; then
y < k + 1
by S3, XXREAL_0:1;
then
y <= k
by NAT_1:13;
then Q7:
y in Seg k
by S3;
dom F1 = Seg k
by A3, A4, FINSEQ_1:def 3;
then Q5:
y in dom p
by Q7, FUNCT_2:def 1;
Q6:
x in dom p
by Q4, FUNCT_2:def 1;
hence
x1 = x2
by Q6, Q5, R0;
verum end; end; then T:
B is
one-to-one
by FUNCT_2:19;
now for x being object holds
( x in dom G iff x in rng B )let x be
object ;
( x in dom G iff x in rng B )now ( x in dom G implies x in rng B )assume U0:
x in dom G
;
x in rng Bthen U1:
x in Seg (k + 1)
by III, FINSEQ_1:def 3;
U2:
dom F = Seg (k + 1)
by A3, FINSEQ_1:def 3;
then U2a:
dom F = dom G
by III, FINSEQ_1:def 3;
reconsider x1 =
x as
Element of
dom F by U2, U0, III, FINSEQ_1:def 3;
U3:
( 1
<= x1 &
x1 <= k + 1 )
by U1, FINSEQ_1:1;
U8:
dom B = dom F
by FUNCT_2:def 1;
dom p = dom F1
by FUNCT_2:def 1;
then Q3:
dom p =
Seg k
by A3, A4, FINSEQ_1:def 3
.=
dom G1
by II, FINSEQ_1:def 3
;
Q4:
Seg k = dom G1
by II, FINSEQ_1:def 3;
per cases
( x1 = j or x1 <> j )
;
suppose Q1:
x1 <> j
;
x in rng Bnow x in rng Bper cases
( x1 <= j or x1 > j )
;
suppose QQ:
x1 <= j
;
x in rng Bthen QQQ:
x1 < j
by Q1, XXREAL_0:1;
j <= k + 1
by U2, FINSEQ_1:1, U2a;
then
x1 < k + 1
by QQQ, XXREAL_0:2;
then
x1 <= k
by NAT_1:13;
then
x1 in rng p
by U3, Q4, R1;
then consider i being
object such that M:
(
i in dom p &
p . i = x1 )
by FUNCT_1:def 3;
reconsider i =
i as
Element of
dom p by M;
i in dom G1
by Q3;
then
i in Seg k
by II, FINSEQ_1:def 3;
then H:
( 1
<= i &
i <= k )
by FINSEQ_1:1;
N:
p . i < j
by M, QQ, Q1, XXREAL_0:1;
k <= k + 1
by NAT_1:11;
then
i <= k + 1
by H, XXREAL_0:2;
then
i in Seg (k + 1)
by H;
then reconsider i =
i as
Element of
dom F by A3, FINSEQ_1:def 3;
i <> k + 1
by H, NAT_1:19;
then
B . i = x1
by M, N, P2;
hence
x in rng B
by U8, FUNCT_1:def 3;
verum end; suppose QQ:
x1 > j
;
x in rng BQQ1:
( 1
<= j &
j <= k + 1 )
by U2, FINSEQ_1:1, U2a;
QQ2:
x1 - 1
<= (k + 1) - 1
by U3, XREAL_1:9;
1
< x1
by QQ, QQ1, XXREAL_0:2;
then
1
+ 1
<= x1
by INT_1:7;
then
(1 + 1) - 1
<= x1 - 1
by XREAL_1:9;
then
x1 - 1
in rng p
by QQ2, Q4, R1, QQ;
then consider i being
object such that M:
(
i in dom p &
p . i = x1 - 1 )
by FUNCT_1:def 3;
reconsider i =
i as
Element of
dom p by M;
i in dom G1
by Q3;
then
i in Seg k
by II, FINSEQ_1:def 3;
then H:
( 1
<= i &
i <= k )
by FINSEQ_1:1;
j + 1
<= x1
by QQ, INT_1:7;
then N:
(j + 1) - 1
<= x1 - 1
by XREAL_1:9;
k <= k + 1
by NAT_1:11;
then
i <= k + 1
by H, XXREAL_0:2;
then
i in Seg (k + 1)
by H;
then reconsider i =
i as
Element of
dom F by A3, FINSEQ_1:def 3;
i <> k + 1
by H, NAT_1:19;
then B . i =
(p . i) + 1
by M, N, P2
.=
x1
by M
;
hence
x in rng B
by U8, FUNCT_1:def 3;
verum end; hence
x in rng B
;
verum end; hence
(
x in dom G iff
x in rng B )
;
verum end; then
B is
onto
by TARSKI:2, FUNCT_2:def 3;
hence
B is
bijective
by T;
for i being Element of dom F holds G . (B . i) is_associated_to F . ithus
for
i being
Element of
dom F holds
G . (B . i) is_associated_to F . i
verumproof
let i be
Element of
dom F;
G . (B . i) is_associated_to F . i
dom F = Seg (k + 1)
by A3, FINSEQ_1:def 3;
then Q0:
( 1
<= i &
i <= k + 1 )
by FINSEQ_1:1;
per cases
( i = k + 1 or i <> k + 1 )
;
suppose Q1:
i <> k + 1
;
G . (B . i) is_associated_to F . ithen
i < k + 1
by Q0, XXREAL_0:1;
then
i <= k
by NAT_1:13;
then Q2:
i in Seg k
by Q0;
i in dom F1
by Q2, A3, A4, FINSEQ_1:def 3;
then
p . i in dom G1
by R1, FUNCT_2:4;
then V:
( 1
<= p . i &
p . i <= k )
by III, LG1, LG3, FINSEQ_1:1;
reconsider if1 =
i as
Element of
dom F1 by Q2, A3, A4, FINSEQ_1:def 3;
hence
G . (B . i) is_associated_to F . i
;
verum end;
end; end; end;
hence
S1[
k + 1]
;
verum
end;
I:
for k being Nat holds S1[k]
from NAT_1:sch 2(A0, A1);
ex n being Nat st len F = n
;
hence
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 AS, I; verum