let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; for F, G being FinSequence of the carrier of V
for f being Permutation of (dom F) st len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
Sum F = Sum G
let F, G be FinSequence of the carrier of V; for f being Permutation of (dom F) st len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
Sum F = Sum G
let f be Permutation of (dom F); ( len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) implies Sum F = Sum G )
defpred S1[ Element of NAT ] means for H1, H2 being FinSequence of the carrier of V st len H1 = $1 & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2;
now let k be
Element of
NAT ;
( ( for H1, H2 being FinSequence of the carrier of V st len H1 = k & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 ) implies for H1, H2 being FinSequence of the carrier of V st len H1 = k + 1 & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 )assume A1:
for
H1,
H2 being
FinSequence of the
carrier of
V st
len H1 = k &
len H1 = len H2 holds
for
f being
Permutation of
(dom H1) st ( for
i being
Element of
NAT st
i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2
;
for H1, H2 being FinSequence of the carrier of V st len H1 = k + 1 & len H1 = len H2 holds
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2let H1,
H2 be
FinSequence of the
carrier of
V;
( len H1 = k + 1 & len H1 = len H2 implies for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 )assume that A2:
len H1 = k + 1
and A3:
len H1 = len H2
;
for f being Permutation of (dom H1) st ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2reconsider p =
H2 | (Seg k) as
FinSequence of the
carrier of
V by FINSEQ_1:18;
let f be
Permutation of
(dom H1);
( ( for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ) implies Sum H1 = Sum H2 )A4:
dom H1 = Seg (k + 1)
by A2, FINSEQ_1:def 3;
then A5:
rng f = Seg (k + 1)
by FUNCT_2:def 3;
A7:
dom H2 = Seg (k + 1)
by A2, A3, FINSEQ_1:def 3;
then reconsider v =
H2 . (k + 1) as
Element of
V by FINSEQ_1:4, FUNCT_1:102;
A8:
dom p = Seg (len p)
by FINSEQ_1:def 3;
(
Seg (k + 1) = {} implies
Seg (k + 1) = {} )
;
then A9:
dom f = Seg (k + 1)
by A4, FUNCT_2:def 1;
A10:
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then A11:
f . (k + 1) in Seg (k + 1)
by A9, A5, FUNCT_1:def 3;
then reconsider n =
f . (k + 1) as
Element of
NAT ;
A12:
n <= k + 1
by A11, FINSEQ_1:1;
then consider m2 being
Nat such that A13:
n + m2 = k + 1
by NAT_1:10;
defpred S2[
Nat,
set ]
means $2
= H1 . (n + $1);
1
<= n
by A11, FINSEQ_1:1;
then consider m1 being
Nat such that A14:
1
+ m1 = n
by NAT_1:10;
reconsider m1 =
m1,
m2 =
m2 as
Element of
NAT by ORDINAL1:def 12;
A15:
for
j being
Nat st
j in Seg m2 holds
ex
x being
set st
S2[
j,
x]
;
consider q2 being
FinSequence such that A16:
dom q2 = Seg m2
and A17:
for
k being
Nat st
k in Seg m2 holds
S2[
k,
q2 . k]
from FINSEQ_1:sch 1(A15);
rng q2 c= the
carrier of
V
proof
let x be
set ;
TARSKI:def 3 ( not x in rng q2 or x in the carrier of V )
assume
x in rng q2
;
x in the carrier of V
then consider y being
set such that A18:
y in dom q2
and A19:
x = q2 . y
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A16, A18;
1
<= y
by A16, A18, FINSEQ_1:1;
then A20:
1
<= n + y
by NAT_1:12;
y <= m2
by A16, A18, FINSEQ_1:1;
then
n + y <= len H1
by A2, A13, XREAL_1:7;
then
n + y in dom H1
by A20, FINSEQ_3:25;
then reconsider xx =
H1 . (n + y) as
Element of
V by FUNCT_1:102;
xx in the
carrier of
V
;
hence
x in the
carrier of
V
by A16, A17, A18, A19;
verum
end; then reconsider q2 =
q2 as
FinSequence of the
carrier of
V by FINSEQ_1:def 4;
reconsider q1 =
H1 | (Seg m1) as
FinSequence of the
carrier of
V by FINSEQ_1:18;
defpred S3[
set ,
set ]
means ( (
f . $1
in dom q1 implies $2
= f . $1 ) & ( not
f . $1
in dom q1 implies for
l being
Element of
NAT st
l = f . $1 holds
$2
= l - 1 ) );
A21:
k <= k + 1
by NAT_1:12;
then A22:
Seg k c= Seg (k + 1)
by FINSEQ_1:5;
A23:
for
i being
Nat st
i in Seg k holds
ex
y being
set st
S3[
i,
y]
proof
let i be
Nat;
( i in Seg k implies ex y being set st S3[i,y] )
assume A24:
i in Seg k
;
ex y being set st S3[i,y]
hence
ex
y being
set st
S3[
i,
y]
;
verum
end; consider g being
FinSequence such that A26:
dom g = Seg k
and A27:
for
i being
Nat st
i in Seg k holds
S3[
i,
g . i]
from FINSEQ_1:sch 1(A23);
A28:
dom p = Seg k
by A2, A3, A21, FINSEQ_1:17;
m1 <= n
by A14, NAT_1:11;
then A29:
m1 <= k + 1
by A12, XXREAL_0:2;
then A30:
dom q1 = Seg m1
by A2, FINSEQ_1:17;
A31:
now let i,
l be
Element of
NAT ;
( l = f . i & not f . i in dom q1 & i in dom g implies m1 + 2 <= l )assume that A32:
l = f . i
and A33:
not
f . i in dom q1
and A34:
i in dom g
;
m1 + 2 <= lA35:
(
l < 1 or
m1 < l )
by A30, A32, A33, FINSEQ_1:1;
f . i in rng f
by A9, A22, A26, A34, FUNCT_1:def 3;
then
m1 + 1
<= l
by A4, A32, A35, FINSEQ_1:1, NAT_1:13;
then
m1 + 1
< l
by A36, XXREAL_0:1;
then
(m1 + 1) + 1
<= l
by NAT_1:13;
hence
m1 + 2
<= l
;
verum end; A37:
len q1 = m1
by A2, A29, FINSEQ_1:17;
1
+ k = 1
+ (m1 + m2)
by A14, A13;
then A40:
m1 <= k
by NAT_1:11;
A41:
rng g c= dom p
proof
let y be
set ;
TARSKI:def 3 ( not y in rng g or y in dom p )
assume
y in rng g
;
y in dom p
then consider x being
set such that A42:
x in dom g
and A43:
g . x = y
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A26, A42;
now per cases
( f . x in dom q1 or not f . x in dom q1 )
;
suppose A46:
not
f . x in dom q1
;
y in dom preconsider j =
f . x as
Element of
NAT by A9, A22, A6, A26, A42;
A47:
f . x in Seg (k + 1)
by A9, A5, A22, A26, A42, FUNCT_1:def 3;
(
j < 1 or
m1 < j )
by A30, A46, FINSEQ_1:1;
then reconsider l =
j - 1 as
Element of
NAT by A47, FINSEQ_1:1, NAT_1:20;
j <= k + 1
by A47, FINSEQ_1:1;
then A48:
l <= (k + 1) - 1
by XREAL_1:9;
m1 + 2
<= j
by A31, A42, A46;
then A49:
(m1 + 2) - 1
<= l
by XREAL_1:9;
1
<= m1 + 1
by NAT_1:12;
then A50:
1
<= l
by A49, XXREAL_0:2;
g . x = j - 1
by A26, A27, A42, A46;
hence
y in dom p
by A28, A43, A50, A48, FINSEQ_1:1;
verum end;
hence
y in dom p
;
verum
end; set q =
q1 ^ q2;
A51:
len q2 = m2
by A16, FINSEQ_1:def 3;
then A52:
len (q1 ^ q2) = m1 + m2
by A37, FINSEQ_1:22;
then A53:
dom (q1 ^ q2) = Seg k
by A14, A13, FINSEQ_1:def 3;
(
dom p = {} implies
dom p = {} )
;
then reconsider g =
g as
Function of
(dom (q1 ^ q2)),
(dom (q1 ^ q2)) by A28, A53, A26, A41, FUNCT_2:def 1, RELSET_1:4;
A54:
len p = k
by A2, A3, A21, FINSEQ_1:17;
A55:
rng g = dom (q1 ^ q2)
proof
thus
rng g c= dom (q1 ^ q2)
;
XBOOLE_0:def 10 dom (q1 ^ q2) c= rng g
let y be
set ;
TARSKI:def 3 ( not y in dom (q1 ^ q2) or y in rng g )
assume A56:
y in dom (q1 ^ q2)
;
y in rng g
then reconsider j =
y as
Element of
NAT ;
consider x being
set such that A57:
x in dom f
and A58:
f . x = y
by A5, A22, A53, A56, FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A9, A57;
now per cases
( x in dom g or not x in dom g )
;
suppose A59:
x in dom g
;
y in rng gnow per cases
( f . x in dom q1 or not f . x in dom q1 )
;
suppose A60:
not
f . x in dom q1
;
y in rng g
j <= k
by A53, A56, 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 A5, FINSEQ_1:1;
then consider x1 being
set such that A61:
x1 in dom f
and A62:
f . x1 = j + 1
by FUNCT_1:def 3;
A63:
now assume
not
x1 in dom g
;
contradictionthen
x1 in (Seg (k + 1)) \ (Seg k)
by A4, A26, A61, XBOOLE_0:def 5;
then
x1 in {(k + 1)}
by FINSEQ_3:15;
then A64:
j + 1
= m1 + 1
by A14, A62, TARSKI:def 1;
1
<= j
by A53, A56, FINSEQ_1:1;
hence
contradiction
by A30, A58, A60, A64, FINSEQ_1:1;
verum end;
(
j < 1 or
m1 < j )
by A30, A58, A60, FINSEQ_1:1;
then
not
j + 1
<= m1
by A53, A56, FINSEQ_1:1, NAT_1:13;
then
not
f . x1 in dom q1
by A30, A62, FINSEQ_1:1;
then g . x1 =
(j + 1) - 1
by A26, A27, A62, A63
.=
y
;
hence
y in rng g
by A63, FUNCT_1:def 3;
verum end; hence
y in rng g
;
verum suppose A65:
not
x in dom g
;
y in rng g
j <= k
by A53, A56, 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 A5, FINSEQ_1:1;
then consider x1 being
set such that A66:
x1 in dom f
and A67:
f . x1 = j + 1
by FUNCT_1:def 3;
x in (Seg (k + 1)) \ (Seg k)
by A4, A26, A57, A65, XBOOLE_0:def 5;
then
x in {(k + 1)}
by FINSEQ_3:15;
then A68:
x = k + 1
by TARSKI:def 1;
m1 <= j
by A14, A58, A68, XREAL_1:29;
then
not
j + 1
<= m1
by NAT_1:13;
then
not
f . x1 in dom q1
by A30, A67, FINSEQ_1:1;
then g . x1 =
(j + 1) - 1
by A26, A27, A67, A69
.=
y
;
hence
y in rng g
by A69, FUNCT_1:def 3;
verum end;
hence
y in rng g
;
verum
end; assume A70:
for
i being
Element of
NAT st
i in dom H2 holds
H2 . i = H1 . (f . i)
;
Sum H1 = Sum H2then A71:
H2 . (k + 1) = H1 . (f . (k + 1))
by A7, FINSEQ_1:4;
g is
one-to-one
proof
let y1 be
set ;
FUNCT_1:def 4 for b1 being set holds
( not y1 in proj1 g or not b1 in proj1 g or not g . y1 = g . b1 or y1 = b1 )let y2 be
set ;
( not y1 in proj1 g or not y2 in proj1 g or not g . y1 = g . y2 or y1 = y2 )
assume that A78:
y1 in dom g
and A79:
y2 in dom g
and A80:
g . y1 = g . y2
;
y1 = y2
reconsider j1 =
y1,
j2 =
y2 as
Element of
NAT by A26, A78, A79;
A81:
f . y2 in Seg (k + 1)
by A9, A5, A22, A26, A79, FUNCT_1:def 3;
A82:
f . y1 in Seg (k + 1)
by A9, A5, A22, A26, A78, FUNCT_1:def 3;
then reconsider a =
f . y1,
b =
f . y2 as
Element of
NAT by A81;
now per 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 A83:
(
f . y1 in dom q1 & not
f . y2 in dom q1 )
;
y1 = y2then A84:
a <= m1
by A30, FINSEQ_1:1;
(
g . j1 = a &
g . j2 = b - 1 )
by A26, A27, A78, A79, A83;
then A85:
(b - 1) + 1
<= m1 + 1
by A80, A84, XREAL_1:6;
1
<= b
by A81, FINSEQ_1:1;
then A86:
b in Seg (m1 + 1)
by A85, FINSEQ_1:1;
not
b in Seg m1
by A2, A29, A83, FINSEQ_1:17;
then
b in (Seg (m1 + 1)) \ (Seg m1)
by A86, 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 A10, A9, A14, A22, A26, A79, FUNCT_1:def 4;
hence
y1 = y2
by A26, A79, FINSEQ_3:8;
verum end; suppose A87:
( not
f . y1 in dom q1 &
f . y2 in dom q1 )
;
y1 = y2then A88:
b <= m1
by A30, FINSEQ_1:1;
(
g . j1 = a - 1 &
g . j2 = b )
by A26, A27, A78, A79, A87;
then A89:
(a - 1) + 1
<= m1 + 1
by A80, A88, XREAL_1:6;
1
<= a
by A82, FINSEQ_1:1;
then A90:
a in Seg (m1 + 1)
by A89, FINSEQ_1:1;
not
a in Seg m1
by A2, A29, A87, FINSEQ_1:17;
then
a in (Seg (m1 + 1)) \ (Seg m1)
by A90, 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 A10, A9, A14, A22, A26, A78, FUNCT_1:def 4;
hence
y1 = y2
by A26, A78, FINSEQ_3:8;
verum end; suppose A91:
( not
f . y1 in dom q1 & not
f . y2 in dom q1 )
;
y1 = y2then
g . j2 = b - 1
by A26, A27, A79;
then A92:
g . y2 = b + (- 1)
;
g . j1 = a - 1
by A26, A27, A78, A91;
then
g . j1 = a + (- 1)
;
then
a = b
by A80, A92, XCMPLX_1:2;
hence
y1 = y2
by A9, A22, A26, A78, A79, FUNCT_1:def 4;
verum end;
hence
y1 = y2
;
verum
end; then reconsider g =
g as
Permutation of
(dom (q1 ^ q2)) by A55, FUNCT_2:57;
(len (q1 ^ <*v*>)) + (len q2) =
((len q1) + (len <*v*>)) + m2
by A51, FINSEQ_1:22
.=
k + 1
by A14, A13, A37, FINSEQ_1:40
;
then
dom H1 = Seg ((len (q1 ^ <*v*>)) + (len q2))
by A2, FINSEQ_1:def 3;
then A93:
H1 = (q1 ^ <*v*>) ^ q2
by A72, A38, FINSEQ_1:def 7;
now let i be
Element of
NAT ;
( i in dom p implies p . i = (q1 ^ q2) . (g . i) )assume A94:
i in dom p
;
p . i = (q1 ^ q2) . (g . i)then
f . i in rng f
by A9, A22, A28, FUNCT_1:def 3;
then reconsider j =
f . i as
Element of
NAT by A5;
now per cases
( f . i in dom q1 or not f . i in dom q1 )
;
suppose A95:
f . i in dom q1
;
p . i = (q1 ^ q2) . (g . i)then A96:
(
f . i = g . i &
H1 . j = q1 . j )
by A28, A27, A94, FUNCT_1:47;
(
H2 . i = p . i &
H2 . i = H1 . (f . i) )
by A70, A7, A22, A28, A94, FUNCT_1:47;
hence
p . i = (q1 ^ q2) . (g . i)
by A95, A96, FINSEQ_1:def 7;
verum end; suppose A97:
not
f . i in dom q1
;
p . i = (q1 ^ q2) . (g . i)then
m1 + 2
<= j
by A28, A26, A31, A94;
then A98:
(m1 + 2) - 1
<= j - 1
by XREAL_1:9;
m1 < m1 + 1
by XREAL_1:29;
then A99:
m1 < j - 1
by A98, 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;
A100:
not
j1 in dom q1
by A30, A99, FINSEQ_1:1;
A101:
g . i = j - 1
by A28, A27, A94, A97;
then
j - 1
in dom (q1 ^ q2)
by A28, A26, A55, A94, FUNCT_1:def 3;
then consider a being
Nat such that A102:
a in dom q2
and A103:
j1 = (len q1) + a
by A100, FINSEQ_1:25;
A104:
len <*v*> = 1
by FINSEQ_1:39;
A105:
(
H2 . i = p . i &
H2 . i = H1 . (f . i) )
by A70, A7, A22, A28, A94, FUNCT_1:47;
A106:
H1 = q1 ^ (<*v*> ^ q2)
by A93, FINSEQ_1:32;
j in dom H1
by A4, A9, A5, A22, A28, A94, FUNCT_1:def 3;
then consider b being
Nat such that A107:
b in dom (<*v*> ^ q2)
and A108:
j = (len q1) + b
by A97, A106, FINSEQ_1:25;
A109:
H1 . j = (<*v*> ^ q2) . b
by A106, A107, A108, FINSEQ_1:def 7;
A110:
b = 1
+ a
by A103, A108;
(q1 ^ q2) . (j - 1) = q2 . a
by A102, A103, FINSEQ_1:def 7;
hence
p . i = (q1 ^ q2) . (g . i)
by A101, A105, A102, A109, A110, A104, FINSEQ_1:def 7;
verum end; hence
p . i = (q1 ^ q2) . (g . i)
;
verum end; then
Sum p = Sum (q1 ^ q2)
by A1, A14, A13, A54, A52;
then Sum H2 =
(Sum (q1 ^ q2)) + (Sum <*v*>)
by A2, A3, A54, A8, RLVECT_1:38, RLVECT_1:44
.=
((Sum q1) + (Sum q2)) + (Sum <*v*>)
by RLVECT_1:41
.=
(Sum q1) + ((Sum <*v*>) + (Sum q2))
by RLVECT_1:def 3
.=
(Sum q1) + (Sum (<*v*> ^ q2))
by RLVECT_1:41
.=
Sum (q1 ^ (<*v*> ^ q2))
by RLVECT_1:41
.=
Sum H1
by A93, FINSEQ_1:32
;
hence
Sum H1 = Sum H2
;
verum end;
then A111:
for k being Element of NAT st S1[k] holds
S1[k + 1]
;
A112:
S1[ 0 ]
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A112, A111);
hence
( len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) implies Sum F = Sum G )
; verum