let D be non empty set ; for F, G being FinSequence of D
for g being BinOp of D st g is associative & g is commutative holds
for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G
let F, G be FinSequence of D; for g being BinOp of D st g is associative & g is commutative holds
for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G
let g be BinOp of D; ( g is associative & g is commutative implies for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G )
assume that
A1:
g is associative
and
A2:
g is commutative
; for f being Permutation of (dom F) st len F >= 1 & len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G
defpred S1[ Nat] means for H1, H2 being FinSequence of D st len H1 >= 1 & len H1 = $1 & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
g "**" H1 = g "**" H2;
A3:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A4:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
let H1,
H2 be
FinSequence of
D;
( len H1 >= 1 & len H1 = k + 1 & len H1 = len H2 implies for f being Permutation of (dom H1) st ( for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
g "**" H1 = g "**" H2 )
assume that
len H1 >= 1
and A5:
len H1 = k + 1
and A6:
len H1 = len H2
;
for f being Permutation of (dom H1) st ( for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
g "**" H1 = g "**" H2
reconsider p =
H2 | (Seg k) as
FinSequence of
D by FINSEQ_1:18;
let f be
Permutation of
(dom H1);
( ( for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) implies g "**" H1 = g "**" H2 )
A7:
dom H1 = Seg (k + 1)
by A5, FINSEQ_1:def 3;
then A8:
rng f = Seg (k + 1)
by FUNCT_2:def 3;
A10:
rng H2 c= D
by FINSEQ_1:def 4;
A11:
dom f = Seg (k + 1)
by A7, FUNCT_2:def 1;
A12:
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then A13:
f . (k + 1) in Seg (k + 1)
by A11, A8, FUNCT_1:def 3;
then reconsider n =
f . (k + 1) as
Element of
NAT ;
A14:
dom H2 = Seg (k + 1)
by A5, A6, FINSEQ_1:def 3;
then
H2 . (k + 1) in rng H2
by A12, FUNCT_1:def 3;
then reconsider d =
H2 . (k + 1) as
Element of
D by A10;
A15:
n <= k + 1
by A13, FINSEQ_1:1;
then consider m2 being
Nat such that A16:
n + m2 = k + 1
by NAT_1:10;
defpred S2[
Nat,
object ]
means $2
= H1 . (n + $1);
1
<= n
by A13, FINSEQ_1:1;
then consider m1 being
Nat such that A17:
1
+ m1 = n
by NAT_1:10;
reconsider m1 =
m1,
m2 =
m2 as
Element of
NAT by ORDINAL1:def 12;
A18:
for
j being
Nat st
j in Seg m2 holds
ex
x being
object st
S2[
j,
x]
;
consider q2 being
FinSequence such that A19:
dom q2 = Seg m2
and A20:
for
k being
Nat st
k in Seg m2 holds
S2[
k,
q2 . k]
from FINSEQ_1:sch 1(A18);
rng q2 c= D
proof
let x be
object ;
TARSKI:def 3 ( not x in rng q2 or x in D )
assume
x in rng q2
;
x in D
then consider y being
object such that A21:
y in findom q2
and A22:
x = q2 . y
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A21, SETWISEO:9;
1
<= y
by A19, A21, FINSEQ_1:1;
then A23:
1
<= n + y
by NAT_1:12;
y <= m2
by A19, A21, FINSEQ_1:1;
then
n + y <= len H1
by A5, A16, XREAL_1:7;
then
n + y in Seg (len H1)
by A23, FINSEQ_1:1;
then
n + y in dom H1
by FINSEQ_1:def 3;
then A24:
H1 . (n + y) in rng H1
by FUNCT_1:def 3;
rng H1 c= D
by FINSEQ_1:def 4;
then reconsider xx =
H1 . (n + y) as
Element of
D by A24;
xx in D
;
hence
x in D
by A19, A20, A21, A22;
verum
end;
then reconsider q2 =
q2 as
FinSequence of
D by FINSEQ_1:def 4;
reconsider q1 =
H1 | (Seg m1) as
FinSequence of
D by FINSEQ_1:18;
defpred S3[
Nat,
object ]
means ( (
f . $1
in dom q1 implies $2
= f . $1 ) & ( not
f . $1
in dom q1 implies for
l being
Nat st
l = f . $1 holds
$2
= l - 1 ) );
A25:
k <= k + 1
by NAT_1:12;
then A26:
Seg k c= Seg (k + 1)
by FINSEQ_1:5;
A27:
for
i being
Nat st
i in Seg k holds
ex
y being
object st
S3[
i,
y]
proof
let i be
Nat;
( i in Seg k implies ex y being object st S3[i,y] )
assume A28:
i in Seg k
;
ex y being object st S3[i,y]
now ( not f . i in dom q1 implies ex y being set st
( ( f . i in dom q1 implies y = f . i ) & ( not f . i in dom q1 implies for t being Nat st t = f . i holds
y = t - 1 ) ) )end;
hence
ex
y being
object st
S3[
i,
y]
;
verum
end;
consider gg being
FinSequence such that A30:
dom gg = Seg k
and A31:
for
i being
Nat st
i in Seg k holds
S3[
i,
gg . i]
from FINSEQ_1:sch 1(A27);
A32:
dom p = Seg k
by A5, A6, A25, FINSEQ_1:17;
m1 <= n
by A17, NAT_1:11;
then A33:
m1 <= k + 1
by A15, XXREAL_0:2;
then A34:
dom q1 = Seg m1
by A5, FINSEQ_1:17;
A35:
now for i, l being Nat st l = f . i & not f . i in dom q1 & i in dom gg holds
m1 + 2 <= llet i,
l be
Nat;
( l = f . i & not f . i in dom q1 & i in dom gg implies m1 + 2 <= l )assume that A36:
l = f . i
and A37:
not
f . i in dom q1
and A38:
i in dom gg
;
m1 + 2 <= lA39:
(
l < 1 or
m1 < l )
by A34, A36, A37, FINSEQ_1:1;
A40:
now not m1 + 1 = lend;
f . i in rng f
by A11, A26, A30, A38, FUNCT_1:def 3;
then
m1 + 1
<= l
by A8, A36, A39, FINSEQ_1:1, NAT_1:13;
then
m1 + 1
< l
by A40, XXREAL_0:1;
then
(m1 + 1) + 1
<= l
by NAT_1:13;
hence
m1 + 2
<= l
;
verum end;
1
+ k = 1
+ (m1 + m2)
by A17, A16;
then A41:
m1 <= k
by NAT_1:11;
A42:
rng gg c= dom p
proof
let y be
object ;
TARSKI:def 3 ( not y in rng gg or y in dom p )
assume
y in rng gg
;
y in dom p
then consider x being
object such that A43:
x in findom gg
and A44:
gg . x = y
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A43, SETWISEO:9;
now y in dom pper cases
( f . x in dom q1 or not f . x in dom q1 )
;
suppose A47:
not
f . x in dom q1
;
y in dom preconsider j =
f . x as
Element of
NAT by A11, A26, A9, A30, A43;
A48:
f . x in Seg (k + 1)
by A11, A8, A26, A30, A43, FUNCT_1:def 3;
(
j < 1 or
m1 < j )
by A34, A47, FINSEQ_1:1;
then reconsider l =
j - 1 as
Element of
NAT by A48, FINSEQ_1:1, NAT_1:20;
j <= k + 1
by A48, FINSEQ_1:1;
then A49:
l <= (k + 1) - 1
by XREAL_1:9;
m1 + 2
<= j
by A35, A43, A47;
then A50:
(m1 + 2) - 1
<= l
by XREAL_1:9;
1
<= m1 + 1
by NAT_1:12;
then A51:
1
<= l
by A50, XXREAL_0:2;
gg . x = j - 1
by A30, A31, A43, A47;
hence
y in dom p
by A32, A44, A51, A49, FINSEQ_1:1;
verum end; end; end;
hence
y in dom p
;
verum
end;
A52:
len q1 = m1
by A5, A33, FINSEQ_1:17;
set q =
q1 ^ q2;
A55:
len q2 = m2
by A19, FINSEQ_1:def 3;
then A56:
len (q1 ^ q2) = m1 + m2
by A52, FINSEQ_1:22;
then A57:
dom (q1 ^ q2) = Seg k
by A17, A16, FINSEQ_1:def 3;
then reconsider gg =
gg as
Function of
(dom (q1 ^ q2)),
(dom (q1 ^ q2)) by A32, A30, A42, FUNCT_2:2;
A58:
len p = k
by A5, A6, A25, FINSEQ_1:17;
A59:
rng gg = dom (q1 ^ q2)
proof
thus
rng gg c= dom (q1 ^ q2)
by A17, A16, A56, A32, A42, FINSEQ_1:def 3;
XBOOLE_0:def 10 dom (q1 ^ q2) c= rng gg
let y be
object ;
TARSKI:def 3 ( not y in dom (q1 ^ q2) or y in rng gg )
assume A60:
y in dom (q1 ^ q2)
;
y in rng gg
then reconsider j =
y as
Element of
NAT ;
consider x being
object such that A61:
x in dom f
and A62:
f . x = y
by A8, A26, A57, A60, FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A11, A61;
now y in rng ggper cases
( x in dom gg or not x in dom gg )
;
suppose A63:
x in dom gg
;
y in rng ggnow y in rng ggper cases
( f . x in dom q1 or not f . x in dom q1 )
;
suppose A64:
not
f . x in dom q1
;
y in rng gg
j <= k
by A57, A60, FINSEQ_1:1;
then
( 1
<= j + 1 &
j + 1
<= k + 1 )
by NAT_1:12, XREAL_1:7;
then
j + 1
in rng f
by A8, FINSEQ_1:1;
then consider x1 being
object such that A65:
x1 in dom f
and A66:
f . x1 = j + 1
by FUNCT_1:def 3;
A67:
now x1 in dom ggassume
not
x1 in dom gg
;
contradictionthen
x1 in (Seg (k + 1)) \ (Seg k)
by A7, A30, A65, XBOOLE_0:def 5;
then
x1 in {(k + 1)}
by FINSEQ_3:15;
then A68:
j + 1
= m1 + 1
by A17, A66, TARSKI:def 1;
1
<= j
by A57, A60, FINSEQ_1:1;
hence
contradiction
by A34, A62, A64, A68, FINSEQ_1:1;
verum end;
(
j < 1 or
m1 < j )
by A34, A62, A64, FINSEQ_1:1;
then
not
j + 1
<= m1
by A57, A60, FINSEQ_1:1, NAT_1:13;
then
not
f . x1 in dom q1
by A34, A66, FINSEQ_1:1;
then gg . x1 =
(j + 1) - 1
by A30, A31, A66, A67
.=
y
;
hence
y in rng gg
by A67, FUNCT_1:def 3;
verum end; end; end; hence
y in rng gg
;
verum end; suppose A69:
not
x in dom gg
;
y in rng gg
j <= k
by A57, A60, FINSEQ_1:1;
then
( 1
<= j + 1 &
j + 1
<= k + 1 )
by NAT_1:12, XREAL_1:7;
then
j + 1
in rng f
by A8, FINSEQ_1:1;
then consider x1 being
object such that A70:
x1 in dom f
and A71:
f . x1 = j + 1
by FUNCT_1:def 3;
x in (Seg (k + 1)) \ (Seg k)
by A7, A30, A61, A69, XBOOLE_0:def 5;
then
x in {(k + 1)}
by FINSEQ_3:15;
then A72:
x = k + 1
by TARSKI:def 1;
m1 <= j
by A17, A62, A72, XREAL_1:29;
then
not
j + 1
<= m1
by NAT_1:13;
then
not
f . x1 in dom q1
by A34, A71, FINSEQ_1:1;
then gg . x1 =
(j + 1) - 1
by A30, A31, A71, A73
.=
y
;
hence
y in rng gg
by A73, FUNCT_1:def 3;
verum end; end; end;
hence
y in rng gg
;
verum
end;
assume A74:
for
i being
Nat st
i in dom H2 holds
H2 . i = H1 . (f . i)
;
g "**" H1 = g "**" H2
then A75:
H2 . (k + 1) = H1 . (f . (k + 1))
by A14, FINSEQ_1:4;
gg is
one-to-one
proof
let y1,
y2 be
object ;
FUNCT_1:def 4 ( not y1 in findom gg or not y2 in findom gg or not gg . y1 = gg . y2 or y1 = y2 )
assume that A82:
y1 in dom gg
and A83:
y2 in dom gg
and A84:
gg . y1 = gg . y2
;
y1 = y2
reconsider j1 =
y1,
j2 =
y2 as
Element of
NAT by A30, A82, A83;
A85:
f . y2 in Seg (k + 1)
by A11, A8, A26, A30, A83, FUNCT_1:def 3;
A86:
f . y1 in Seg (k + 1)
by A11, A8, A26, A30, A82, FUNCT_1:def 3;
then reconsider a =
f . y1,
b =
f . y2 as
Element of
NAT by A85;
now y1 = y2per cases
( ( f . y1 in dom q1 & f . y2 in dom q1 ) or ( f . y1 in dom q1 & not f . y2 in dom q1 ) or ( not f . y1 in dom q1 & f . y2 in dom q1 ) or ( not f . y1 in dom q1 & not f . y2 in dom q1 ) )
;
suppose A87:
(
f . y1 in dom q1 & not
f . y2 in dom q1 )
;
y1 = y2then A88:
a <= m1
by A34, FINSEQ_1:1;
(
gg . j1 = a &
gg . j2 = b - 1 )
by A30, A31, A82, A83, A87;
then A89:
(b - 1) + 1
<= m1 + 1
by A84, A88, XREAL_1:6;
1
<= b
by A85, FINSEQ_1:1;
then A90:
b in Seg (m1 + 1)
by A89, FINSEQ_1:1;
not
b in Seg m1
by A5, A33, A87, FINSEQ_1:17;
then
b in (Seg (m1 + 1)) \ (Seg m1)
by A90, XBOOLE_0:def 5;
then
b in {(m1 + 1)}
by FINSEQ_3:15;
then
b = m1 + 1
by TARSKI:def 1;
then
y2 = k + 1
by A12, A11, A17, A26, A30, A83, FUNCT_1:def 4;
hence
y1 = y2
by A30, A83, FINSEQ_3:8;
verum end; suppose A91:
( not
f . y1 in dom q1 &
f . y2 in dom q1 )
;
y1 = y2then A92:
b <= m1
by A34, FINSEQ_1:1;
(
gg . j1 = a - 1 &
gg . j2 = b )
by A30, A31, A82, A83, A91;
then A93:
(a - 1) + 1
<= m1 + 1
by A84, A92, XREAL_1:6;
1
<= a
by A86, FINSEQ_1:1;
then A94:
a in Seg (m1 + 1)
by A93, FINSEQ_1:1;
not
a in Seg m1
by A5, A33, A91, FINSEQ_1:17;
then
a in (Seg (m1 + 1)) \ (Seg m1)
by A94, XBOOLE_0:def 5;
then
a in {(m1 + 1)}
by FINSEQ_3:15;
then
a = m1 + 1
by TARSKI:def 1;
then
y1 = k + 1
by A12, A11, A17, A26, A30, A82, FUNCT_1:def 4;
hence
y1 = y2
by A30, A82, FINSEQ_3:8;
verum end; suppose A95:
( not
f . y1 in dom q1 & not
f . y2 in dom q1 )
;
y1 = y2then
gg . j2 = b - 1
by A30, A31, A83;
then A96:
gg . y2 = b + (- 1)
;
gg . j1 = a - 1
by A30, A31, A82, A95;
then
gg . j1 = a + (- 1)
;
then
a = b
by A84, A96, XCMPLX_1:2;
hence
y1 = y2
by A11, A26, A30, A82, A83, FUNCT_1:def 4;
verum end; end; end;
hence
y1 = y2
;
verum
end;
then reconsider gg =
gg as
Permutation of
(dom (q1 ^ q2)) by A59, FUNCT_2:57;
(len (q1 ^ <*d*>)) + (len q2) =
((len q1) + (len <*d*>)) + m2
by A55, FINSEQ_1:22
.=
k + 1
by A17, A16, A52, FINSEQ_1:40
;
then
dom H1 = Seg ((len (q1 ^ <*d*>)) + (len q2))
by A5, FINSEQ_1:def 3;
then A97:
H1 = (q1 ^ <*d*>) ^ q2
by A76, A53, FINSEQ_1:def 7;
A98:
now for i being Nat st i in dom p holds
p . i = (q1 ^ q2) . (gg . i)let i be
Nat;
( i in dom p implies p . i = (q1 ^ q2) . (gg . i) )assume A99:
i in dom p
;
p . i = (q1 ^ q2) . (gg . i)then
f . i in rng f
by A11, A26, A32, FUNCT_1:def 3;
then reconsider j =
f . i as
Element of
NAT by A8;
now p . i = (q1 ^ q2) . (gg . i)per cases
( f . i in dom q1 or not f . i in dom q1 )
;
suppose A100:
f . i in dom q1
;
p . i = (q1 ^ q2) . (gg . i)then A101:
(
f . i = gg . i &
H1 . j = q1 . j )
by A32, A31, A99, FUNCT_1:47;
(
H2 . i = p . i &
H2 . i = H1 . (f . i) )
by A74, A14, A26, A32, A99, FUNCT_1:47;
hence
p . i = (q1 ^ q2) . (gg . i)
by A100, A101, FINSEQ_1:def 7;
verum end; suppose A102:
not
f . i in dom q1
;
p . i = (q1 ^ q2) . (gg . i)then
m1 + 2
<= j
by A32, A30, A35, A99;
then A103:
(m1 + 2) - 1
<= j - 1
by XREAL_1:9;
m1 < m1 + 1
by XREAL_1:29;
then A104:
m1 < j - 1
by A103, XXREAL_0:2;
then
m1 < j
by XREAL_1:146, XXREAL_0:2;
then reconsider j1 =
j - 1 as
Element of
NAT by NAT_1:20;
A105:
not
j1 in dom q1
by A34, A104, FINSEQ_1:1;
A106:
gg . i = j - 1
by A32, A31, A99, A102;
then
j - 1
in dom (q1 ^ q2)
by A32, A30, A59, A99, FUNCT_1:def 3;
then consider a being
Nat such that A107:
a in dom q2
and A108:
j1 = (len q1) + a
by A105, FINSEQ_1:25;
A109:
len <*d*> = 1
by FINSEQ_1:39;
A110:
(
H2 . i = p . i &
H2 . i = H1 . (f . i) )
by A74, A14, A26, A32, A99, FUNCT_1:47;
A111:
H1 = q1 ^ (<*d*> ^ q2)
by A97, FINSEQ_1:32;
j in dom H1
by A7, A11, A8, A26, A32, A99, FUNCT_1:def 3;
then consider b being
Nat such that A112:
b in dom (<*d*> ^ q2)
and A113:
j = (len q1) + b
by A102, A111, FINSEQ_1:25;
A114:
H1 . j = (<*d*> ^ q2) . b
by A111, A112, A113, FINSEQ_1:def 7;
A115:
b = 1
+ a
by A108, A113;
(q1 ^ q2) . (j - 1) = q2 . a
by A107, A108, FINSEQ_1:def 7;
hence
p . i = (q1 ^ q2) . (gg . i)
by A106, A110, A107, A114, A115, A109, FINSEQ_1:def 7;
verum end; end; end; hence
p . i = (q1 ^ q2) . (gg . i)
;
verum end;
now g "**" H1 = g "**" H2per cases
( len p <> 0 or len p = 0 )
;
suppose A116:
len p <> 0
;
g "**" H1 = g "**" H2A117:
H2 = p ^ <*d*>
by A5, A6, FINSEQ_3:55;
g "**" p = g "**" (q1 ^ q2)
by A4, A17, A16, A58, A56, A98, A116, NAT_1:14;
then A118:
g "**" H2 = g . (
(g "**" (q1 ^ q2)),
d)
by A116, A117, Th4, NAT_1:14;
now g "**" H1 = g "**" H2per cases
( ( len q1 <> 0 & len q2 <> 0 ) or ( len q1 = 0 & len q2 <> 0 ) or ( len q1 <> 0 & len q2 = 0 ) or ( len q1 = 0 & len q2 = 0 ) )
;
suppose A119:
(
len q1 <> 0 &
len q2 <> 0 )
;
g "**" H1 = g "**" H2
(
len (<*d*> ^ q2) = (len <*d*>) + (len q2) &
len <*d*> = 1 )
by FINSEQ_1:22, FINSEQ_1:40;
then A120:
len (<*d*> ^ q2) >= 1
by NAT_1:12;
A121:
len q1 >= 1
by A119, NAT_1:14;
len q2 >= 1
by A119, NAT_1:14;
then g "**" H2 =
g . (
(g . ((g "**" q1),(g "**" q2))),
d)
by A1, A118, A121, Th5
.=
g . (
(g "**" q1),
(g . ((g "**" q2),d)))
by A1, BINOP_1:def 3
.=
g . (
(g "**" q1),
(g . (d,(g "**" q2))))
by A2, BINOP_1:def 2
.=
g . (
(g "**" q1),
(g "**" (<*d*> ^ q2)))
by A1, A119, Th6, NAT_1:14
.=
g "**" (q1 ^ (<*d*> ^ q2))
by A1, A121, A120, Th5
.=
g "**" H1
by A97, FINSEQ_1:32
;
hence
g "**" H1 = g "**" H2
;
verum end; suppose
(
len q1 = 0 &
len q2 <> 0 )
;
g "**" H1 = g "**" H2then A122:
q1 = {}
;
then A123:
H1 =
<*d*> ^ q2
by A97, FINSEQ_1:34
.=
<*d*> ^ (q1 ^ q2)
by A122, FINSEQ_1:34
;
g "**" H2 =
g . (
d,
(g "**" (q1 ^ q2)))
by A2, A118, BINOP_1:def 2
.=
g "**" (<*d*> ^ (q1 ^ q2))
by A1, A17, A16, A58, A56, A116, Th6, NAT_1:14
;
hence
g "**" H1 = g "**" H2
by A123;
verum end; end; end; hence
g "**" H1 = g "**" H2
;
verum end; suppose A125:
len p = 0
;
g "**" H1 = g "**" H2then
dom H1 = {1}
by A5, A58, FINSEQ_1:2, FINSEQ_1:def 3;
then A126:
(
dom f = {1} &
rng f = {1} )
by FUNCT_2:def 1, FUNCT_2:def 3;
1
in {1}
by TARSKI:def 1;
then
f . 1
in {1}
by A126, FUNCT_1:def 3;
then
H1 . 1
= H2 . 1
by A75, A58, A125, TARSKI:def 1;
then
H1 = <*d*>
by A5, A58, A125, FINSEQ_1:40;
hence
g "**" H1 = g "**" H2
by A5, A6, A58, A125, FINSEQ_1:40;
verum end; end; end;
hence
g "**" H1 = g "**" H2
;
verum
end; end;
let f be Permutation of (dom F); ( len F >= 1 & len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) implies g "**" F = g "**" G )
A127:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A127, A3);
hence
( len F >= 1 & len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) implies g "**" F = g "**" G )
; verum