let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: 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 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; :: thesis: for f being Permutation of (dom F) st len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) holds
Sum F = Sum G

let f be Permutation of (dom F); :: thesis: ( len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) implies Sum F = Sum G )

defpred S1[ 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 Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2;
now :: thesis: for k being Nat st ( 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 Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 ) holds
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 Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2
let k be Nat; :: thesis: ( ( 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 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 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 Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 ; :: thesis: 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 Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2

let H1, H2 be FinSequence of the carrier of V; :: thesis: ( 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
Sum H1 = Sum H2 )

assume that
A2: len H1 = k + 1 and
A3: len H1 = len H2 ; :: thesis: for f being Permutation of (dom H1) st ( for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2

reconsider p = H2 | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;
let f be Permutation of (dom H1); :: thesis: ( ( for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) implies Sum H1 = Sum H2 )

A4: dom H1 = Seg (k + 1) by ;
then A5: rng f = Seg (k + 1) by FUNCT_2:def 3;
A6: now :: thesis: for n being Nat st n in dom f holds
f . n is Element of NAT
let n be Nat; :: thesis: ( n in dom f implies f . n is Element of NAT )
assume n in dom f ; :: thesis: f . n is Element of NAT
then f . n in Seg (k + 1) by ;
hence f . n is Element of NAT ; :: thesis: verum
end;
A7: dom H2 = Seg (k + 1) by ;
then reconsider v = H2 . (k + 1) as Element of V by ;
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 ;
A10: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A11: f . (k + 1) in Seg (k + 1) by ;
then reconsider n = f . (k + 1) as Element of NAT ;
A12: n <= k + 1 by ;
then consider m2 being Nat such that
A13: n + m2 = k + 1 by NAT_1:10;
defpred S2[ Nat, object ] means \$2 = H1 . (n + \$1);
1 <= n by ;
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 object 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 rng q2 c= the carrier of V
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng q2 or x in the carrier of V )
assume x in rng q2 ; :: thesis: x in the carrier of V
then consider y being object 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 A18;
1 <= y by ;
then A20: 1 <= n + y by NAT_1:12;
y <= m2 by ;
then n + y <= len H1 by ;
then n + y in dom H1 by ;
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; :: thesis: 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 , 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 ) );
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 object st S3[i,y]
proof
let i be Nat; :: thesis: ( i in Seg k implies ex y being object st S3[i,y] )
assume A24: i in Seg k ; :: thesis: ex y being object st S3[i,y]
now :: thesis: ( 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 ) ) )
f . i in Seg (k + 1) by ;
then reconsider j = f . i as Element of NAT ;
assume A25: not f . i in dom q1 ; :: thesis: 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 ) )

take y = j - 1; :: thesis: ( ( 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 ) )

thus ( f . i in dom q1 implies y = f . i ) by A25; :: thesis: ( not f . i in dom q1 implies for t being Nat st t = f . i holds
y = t - 1 )

assume not f . i in dom q1 ; :: thesis: for t being Nat st t = f . i holds
y = t - 1

let t be Nat; :: thesis: ( t = f . i implies y = t - 1 )
assume t = f . i ; :: thesis: y = t - 1
hence y = t - 1 ; :: thesis: verum
end;
hence ex y being object st S3[i,y] ; :: thesis: 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 A28: dom p = Seg k by ;
m1 <= n by ;
then A29: m1 <= k + 1 by ;
then A30: dom q1 = Seg m1 by ;
A31: now :: thesis: for i, l being Nat st l = f . i & not f . i in dom q1 & i in dom g holds
m1 + 2 <= l
let i, l be Nat; :: thesis: ( 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 ; :: thesis: m1 + 2 <= l
A35: ( l < 1 or m1 < l ) by ;
A36: now :: thesis: not m1 + 1 = l
assume m1 + 1 = l ; :: thesis: contradiction
then k + 1 = i by ;
then k + 1 <= k + 0 by ;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
f . i in rng f by ;
then m1 + 1 <= l by ;
then m1 + 1 < l by ;
then (m1 + 1) + 1 <= l by NAT_1:13;
hence m1 + 2 <= l ; :: thesis: verum
end;
A37: len q1 = m1 by ;
A38: now :: thesis: for j being Nat st j in dom q2 holds
H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j
let j be Nat; :: thesis: ( j in dom q2 implies H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j )
assume A39: j in dom q2 ; :: thesis: H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j
len (q1 ^ <*v*>) = m1 + () by
.= n by ;
hence H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j by ; :: thesis: verum
end;
1 + k = 1 + (m1 + m2) by ;
then A40: m1 <= k by NAT_1:11;
A41: rng g c= dom p
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in dom p )
assume y in rng g ; :: thesis: y in dom p
then consider x being object 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 A42;
now :: thesis: y in dom p
per cases ( f . x in dom q1 or not f . x in dom q1 ) ;
suppose A44: f . x in dom q1 ; :: thesis: y in dom p
A45: dom q1 c= dom p by ;
f . x = g . x by A26, A27, A42, A44;
hence y in dom p by ; :: thesis: verum
end;
suppose A46: not f . x in dom q1 ; :: thesis: y in dom p
reconsider j = f . x as Element of NAT by A9, A22, A6, A26, A42;
A47: f . x in Seg (k + 1) by ;
( j < 1 or m1 < j ) by ;
then reconsider l = j - 1 as Element of NAT by ;
j <= k + 1 by ;
then A48: l <= (k + 1) - 1 by XREAL_1:9;
m1 + 2 <= j by ;
then A49: (m1 + 2) - 1 <= l by XREAL_1:9;
1 <= m1 + 1 by NAT_1:12;
then A50: 1 <= l by ;
g . x = j - 1 by A26, A27, A42, A46;
hence y in dom p by ; :: thesis: verum
end;
end;
end;
hence y in dom p ; :: thesis: verum
end;
set q = q1 ^ q2;
A51: len q2 = m2 by ;
then A52: len (q1 ^ q2) = m1 + m2 by ;
then A53: dom (q1 ^ q2) = Seg k by ;
then reconsider g = g as Function of (dom (q1 ^ q2)),(dom (q1 ^ q2)) by ;
A54: len p = k by ;
A55: rng g = dom (q1 ^ q2)
proof
thus rng g c= dom (q1 ^ q2) ; :: according to XBOOLE_0:def 10 :: thesis: dom (q1 ^ q2) c= rng g
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (q1 ^ q2) or y in rng g )
assume A56: y in dom (q1 ^ q2) ; :: thesis: y in rng g
then reconsider j = y as Element of NAT ;
consider x being object such that
A57: x in dom f and
A58: f . x = y by ;
reconsider x = x as Element of NAT by ;
now :: thesis: y in rng g
per cases ( x in dom g or not x in dom g ) ;
suppose A59: x in dom g ; :: thesis: y in rng g
now :: thesis: y in rng g
per cases ( f . x in dom q1 or not f . x in dom q1 ) ;
suppose f . x in dom q1 ; :: thesis: y in rng g
then g . x = f . x by ;
hence y in rng g by ; :: thesis: verum
end;
suppose A60: not f . x in dom q1 ; :: thesis: y in rng g
j <= k by ;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by ;
then j + 1 in rng f by ;
then consider x1 being object such that
A61: x1 in dom f and
A62: f . x1 = j + 1 by FUNCT_1:def 3;
A63: now :: thesis: x1 in dom g
assume not x1 in dom g ; :: thesis: contradiction
then x1 in (Seg (k + 1)) \ (Seg k) by ;
then x1 in {(k + 1)} by FINSEQ_3:15;
then A64: j + 1 = m1 + 1 by ;
1 <= j by ;
hence contradiction by A30, A58, A60, A64, FINSEQ_1:1; :: thesis: verum
end;
( j < 1 or m1 < j ) by ;
then not j + 1 <= m1 by ;
then not f . x1 in dom q1 by ;
then g . x1 = (j + 1) - 1 by A26, A27, A62, A63
.= y ;
hence y in rng g by ; :: thesis: verum
end;
end;
end;
hence y in rng g ; :: thesis: verum
end;
suppose A65: not x in dom g ; :: thesis: y in rng g
j <= k by ;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by ;
then j + 1 in rng f by ;
then consider x1 being object 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 ;
then x in {(k + 1)} by FINSEQ_3:15;
then A68: x = k + 1 by TARSKI:def 1;
A69: now :: thesis: x1 in dom g
assume not x1 in dom g ; :: thesis: contradiction
then x1 in (Seg (k + 1)) \ (Seg k) by ;
then x1 in {(k + 1)} by FINSEQ_3:15;
then j + 1 = j + 0 by ;
hence contradiction ; :: thesis: verum
end;
m1 <= j by ;
then not j + 1 <= m1 by NAT_1:13;
then not f . x1 in dom q1 by ;
then g . x1 = (j + 1) - 1 by A26, A27, A67, A69
.= y ;
hence y in rng g by ; :: thesis: verum
end;
end;
end;
hence y in rng g ; :: thesis: verum
end;
assume A70: for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ; :: thesis: Sum H1 = Sum H2
then A71: H2 . (k + 1) = H1 . (f . (k + 1)) by ;
A72: now :: thesis: for j being Nat st j in dom (q1 ^ <*v*>) holds
H1 . j = (q1 ^ <*v*>) . j
let j be Nat; :: thesis: ( j in dom (q1 ^ <*v*>) implies H1 . j = (q1 ^ <*v*>) . j )
assume A73: j in dom (q1 ^ <*v*>) ; :: thesis: H1 . j = (q1 ^ <*v*>) . j
A74: now :: thesis: ( j in Seg m1 implies H1 . j = (q1 ^ <*v*>) . j )
assume j in Seg m1 ; :: thesis: H1 . j = (q1 ^ <*v*>) . j
then A75: j in dom q1 by ;
then q1 . j = H1 . j by FUNCT_1:47;
hence H1 . j = (q1 ^ <*v*>) . j by ; :: thesis: verum
end;
A76: now :: thesis: ( j in {n} implies (q1 ^ <*v*>) . j = H1 . j )
( 1 in Seg 1 & len <*v*> = 1 ) by ;
then 1 in dom <*v*> by FINSEQ_1:def 3;
then A77: (q1 ^ <*v*>) . ((len q1) + 1) = <*v*> . 1 by FINSEQ_1:def 7;
assume j in {n} ; :: thesis: (q1 ^ <*v*>) . j = H1 . j
then j = n by TARSKI:def 1;
hence (q1 ^ <*v*>) . j = H1 . j by ; :: thesis: verum
end;
len (q1 ^ <*v*>) = m1 + () by
.= m1 + 1 by FINSEQ_1:40 ;
then j in Seg (m1 + 1) by ;
then j in (Seg m1) \/ {n} by ;
hence H1 . j = (q1 ^ <*v*>) . j by ; :: thesis: verum
end;
g is one-to-one
proof
let y1, y2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not y1 in dom g or not y2 in dom 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 ; :: thesis: y1 = y2
reconsider j1 = y1, j2 = y2 as Element of NAT by ;
A81: f . y2 in Seg (k + 1) by ;
A82: f . y1 in Seg (k + 1) by ;
then reconsider a = f . y1, b = f . y2 as Element of NAT by A81;
now :: thesis: y1 = y2
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 ( f . y1 in dom q1 & f . y2 in dom q1 ) ; :: thesis: y1 = y2
then ( g . j1 = f . y1 & g . j2 = f . y2 ) by A26, A27, A78, A79;
hence y1 = y2 by ; :: thesis: verum
end;
suppose A83: ( f . y1 in dom q1 & not f . y2 in dom q1 ) ; :: thesis: y1 = y2
then A84: a <= m1 by ;
( g . j1 = a & g . j2 = b - 1 ) by A26, A27, A78, A79, A83;
then A85: (b - 1) + 1 <= m1 + 1 by ;
1 <= b by ;
then A86: b in Seg (m1 + 1) by ;
not b in Seg m1 by ;
then b in (Seg (m1 + 1)) \ (Seg m1) by ;
then b in {(m1 + 1)} by FINSEQ_3:15;
then b = m1 + 1 by TARSKI:def 1;
then y2 = k + 1 by ;
hence y1 = y2 by ; :: thesis: verum
end;
suppose A87: ( not f . y1 in dom q1 & f . y2 in dom q1 ) ; :: thesis: y1 = y2
then A88: b <= m1 by ;
( g . j1 = a - 1 & g . j2 = b ) by A26, A27, A78, A79, A87;
then A89: (a - 1) + 1 <= m1 + 1 by ;
1 <= a by ;
then A90: a in Seg (m1 + 1) by ;
not a in Seg m1 by ;
then a in (Seg (m1 + 1)) \ (Seg m1) by ;
then a in {(m1 + 1)} by FINSEQ_3:15;
then a = m1 + 1 by TARSKI:def 1;
then y1 = k + 1 by ;
hence y1 = y2 by ; :: thesis: verum
end;
suppose A91: ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ; :: thesis: y1 = y2
then g . j2 = b - 1 by ;
then A92: g . y2 = b + (- 1) ;
g . j1 = a - 1 by A26, A27, A78, A91;
then g . j1 = a + (- 1) ;
then a = b by ;
hence y1 = y2 by ; :: thesis: verum
end;
end;
end;
hence y1 = y2 ; :: thesis: verum
end;
then reconsider g = g as Permutation of (dom (q1 ^ q2)) by ;
(len (q1 ^ <*v*>)) + (len q2) = ((len q1) + ()) + m2 by
.= k + 1 by ;
then dom H1 = Seg ((len (q1 ^ <*v*>)) + (len q2)) by ;
then A93: H1 = (q1 ^ <*v*>) ^ q2 by ;
now :: thesis: for i being Nat st i in dom p holds
p . i = (q1 ^ q2) . (g . i)
let i be Nat; :: thesis: ( i in dom p implies p . i = (q1 ^ q2) . (g . i) )
assume A94: i in dom p ; :: thesis: p . i = (q1 ^ q2) . (g . i)
then f . i in rng f by ;
then reconsider j = f . i as Element of NAT by A5;
now :: thesis: p . i = (q1 ^ q2) . (g . i)
per cases ( f . i in dom q1 or not f . i in dom q1 ) ;
suppose A95: f . i in dom q1 ; :: thesis: p . i = (q1 ^ q2) . (g . i)
then A96: ( f . i = g . i & H1 . j = q1 . j ) by ;
( H2 . i = p . i & H2 . i = H1 . (f . i) ) by ;
hence p . i = (q1 ^ q2) . (g . i) by ; :: thesis: verum
end;
suppose A97: not f . i in dom q1 ; :: thesis: 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 ;
then m1 < j by ;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:20;
A100: not j1 in dom q1 by ;
A101: g . i = j - 1 by A28, A27, A94, A97;
then j - 1 in dom (q1 ^ q2) by ;
then consider a being Nat such that
A102: a in dom q2 and
A103: j1 = (len q1) + a by ;
A104: len <*v*> = 1 by FINSEQ_1:39;
A105: ( H2 . i = p . i & H2 . i = H1 . (f . i) ) by ;
A106: H1 = q1 ^ (<*v*> ^ q2) by ;
j in dom H1 by ;
then consider b being Nat such that
A107: b in dom (<*v*> ^ q2) and
A108: j = (len q1) + b by ;
A109: H1 . j = (<*v*> ^ q2) . b by ;
A110: b = 1 + a by ;
(q1 ^ q2) . (j - 1) = q2 . a by ;
hence p . i = (q1 ^ q2) . (g . i) by ; :: thesis: verum
end;
end;
end;
hence p . i = (q1 ^ q2) . (g . i) ; :: thesis: verum
end;
then Sum p = Sum (q1 ^ q2) by A1, A14, A13, A54, A52;
then Sum H2 = (Sum (q1 ^ q2)) + () by
.= ((Sum q1) + (Sum q2)) + () by RLVECT_1:41
.= (Sum q1) + (() + (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 ;
hence Sum H1 = Sum H2 ; :: thesis: verum
end;
then A111: for k being Nat st S1[k] holds
S1[k + 1] ;
A112: S1[ 0 ]
proof
let H1, H2 be FinSequence of the carrier of V; :: thesis: ( len H1 = 0 & 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
Sum H1 = Sum H2 )

assume that
A113: len H1 = 0 and
A114: len H1 = len H2 ; :: thesis: for f being Permutation of (dom H1) st ( for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2

Sum H1 = 0. V by ;
hence for f being Permutation of (dom H1) st ( for i being Nat st i in dom H2 holds
H2 . i = H1 . (f . i) ) holds
Sum H1 = Sum H2 by ; :: thesis: verum
end;
for k being Nat holds S1[k] from hence ( len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (f . i) ) implies Sum F = Sum G ) ; :: thesis: verum