let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis:
let F, G be FinSequence of the carrier of V; :: thesis:
let f be Permutation of dom F; :: thesis:
defpred S₁[ 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;
A1: S₁[ 0 ]

proof

let H1, H2 be FinSequence of the carrier of V; :: thesis:
assume ( len H1 = 0 & len H1 = len H2 ) ; :: thesis:
then ( Sum H1 = 0. V & Sum H2 = 0. V ) by RLVECT_1:94;
hence 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 ; :: thesis:

end;

A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

let k be Element of NAT ; :: thesis:
assume A3: 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 ; :: thesis:
let H1, H2 be FinSequence of the carrier of V; :: thesis:
assume that
A4: len H1 = k + 1 and
A5: len H1 = len H2 ; :: thesis:
let f be Permutation of dom H1; :: thesis:
assume A6: for i being Element of NAT st i in dom H2 holds
H2 . i = H1 . (f . i) ; :: thesis:
reconsider p = H2 | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:23;
A7: k + 1 in Seg (k + 1) by FINSEQ_1:6;
A8: ( dom H2 = Seg (k + 1) & dom H1 = Seg (k + 1) ) by A4, A5, FINSEQ_1:def 3;
( Seg (k + 1) = {} implies Seg (k + 1) = {} ) ;
then A9: ( dom f = Seg (k + 1) & rng f = Seg (k + 1) ) by A8, FUNCT_2:def 1, FUNCT_2:def 3;
then A10: f . (k + 1) in Seg (k + 1) by A7, FUNCT_1:def 5;
then reconsider n = f . (k + 1) as Element of NAT ;
A11: H2 . (k + 1) = H1 . (f . (k + 1)) by A6, A8, FINSEQ_1:6;
reconsider v = H2 . (k + 1) as Element of V by A4, A5, A7, RLVECT_1:54;
1 <= n by A10, FINSEQ_1:3;
then consider m1 being Nat such that
A12: 1 + m1 = n by NAT_1:10;
A13: n <= k + 1 by A10, FINSEQ_1:3;
then consider m2 being Nat such that
A14: n + m2 = k + 1 by NAT_1:10;
reconsider m1 = m1, m2 = m2 as Element of NAT by ORDINAL1:def 13;
reconsider q1 = H1 | (Seg m1) as FinSequence of the carrier of V by FINSEQ_1:23;
defpred S₂[ Nat, set ] means $2 = H1 . (n + $1);
A16: for j being Nat st j in Seg m2 holds
ex x being set st S₂[j,x] ;
consider q2 being FinSequence such that
A17: dom q2 = Seg m2 and
A18: for k being Nat st k in Seg m2 holds
S₂[k,q2 . k] from FINSEQ_1:sch 1(A16);
rng q2 c= the carrier of V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng q2 ; :: thesis:
then consider y being set such that
A19: y in dom q2 and
A20: x = q2 . y by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A17, A19;
( 1 <= y & y <= n + y ) by A17, A19, FINSEQ_1:3, NAT_1:12;
then A21: 1 <= n + y by XXREAL_0:2;
y <= m2 by A17, A19, FINSEQ_1:3;
then n + y <= len H1 by A4, A14, XREAL_1:9;
then n + y in Seg (len H1) by A21, FINSEQ_1:3;
then reconsider xx = H1 . (n + y) as Element of V by RLVECT_1:54;
xx in the carrier of V ;
hence x in the carrier of V by A17, A18, A19, A20; :: thesis:

end;

then reconsider q2 = q2 as FinSequence of the carrier of V by FINSEQ_1:def 4;
set q = q1 ^ q2;
A22: k <= k + 1 by NAT_1:12;
then A23: len p = k by A4, A5, FINSEQ_1:21;
m1 <= n by A12, NAT_1:11;
then A24: m1 <= k + 1 by A13, XXREAL_0:2;
then A25: ( len q1 = m1 & len q2 = m2 ) by A4, A17, FINSEQ_1:21, FINSEQ_1:def 3;
then A26: len (q1 ^ q2) = m1 + m2 by FINSEQ_1:35;
A27: 1 + k = 1 + (m1 + m2) by A12, A14;
(len (q1 ^ <*v*>)) + (len q2) = ((len q1) + (len <*v*>)) + m2 by A25, FINSEQ_1:35
.= k + 1 by A12, A14, A25, FINSEQ_1:57 ;
then A28: dom H1 = Seg ((len (q1 ^ <*v*>)) + (len q2)) by A4, FINSEQ_1:def 3;

A29: now

let j be Nat; :: thesis:
assume A30: j in dom (q1 ^ <*v*>) ; :: thesis:
len (q1 ^ <*v*>) = m1 + (len <*v*>) by A25, FINSEQ_1:35
.= m1 + 1 by FINSEQ_1:57 ;
then j in Seg (m1 + 1) by A30, FINSEQ_1:def 3;
then A31: j in (Seg m1) \/ {n} by A12, FINSEQ_1:11;

A32: now

assume j in Seg m1 ; :: thesis:
then A33: j in dom q1 by A4, A24, FINSEQ_1:21;
then q1 . j = H1 . j by FUNCT_1:70;
hence H1 . j = (q1 ^ <*v*>) . j by A33, FINSEQ_1:def 7; :: thesis:

end;

now

assume j in {n} ; :: thesis:
then A34: j = n by TARSKI:def 1;
( 1 in Seg 1 & len <*v*> = 1 ) by FINSEQ_1:3, FINSEQ_1:56;
then 1 in dom <*v*> by FINSEQ_1:def 3;
then (q1 ^ <*v*>) . ((len q1) + 1) = <*v*> . 1 by FINSEQ_1:def 7;
hence (q1 ^ <*v*>) . j = H1 . j by A11, A12, A25, A34, FINSEQ_1:57; :: thesis:

end;

hence H1 . j = (q1 ^ <*v*>) . j by A31, A32, XBOOLE_0:def 3; :: thesis:

end;

now

let j be Nat; :: thesis:
assume A35: j in dom q2 ; :: thesis:
len (q1 ^ <*v*>) = m1 + (len <*v*>) by A25, FINSEQ_1:35
.= n by A12, FINSEQ_1:56 ;
hence H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j by A17, A18, A35; :: thesis:

end;

then A36: H1 = (q1 ^ <*v*>) ^ q2 by A28, A29, FINSEQ_1:def 7;
A37: m1 <= k by A27, NAT_1:11;
A38: Seg k c= Seg (k + 1) by A22, FINSEQ_1:7;

A39: now

let n be Element of NAT ; :: thesis:
assume n in dom f ; :: thesis:
then f . n in Seg (k + 1) by A9, FUNCT_1:def 5;
hence f . n is Element of NAT ; :: thesis:

end;

A40: dom q1 = Seg m1 by A4, A24, FINSEQ_1:21;
A41: ( dom p = Seg k & dom (q1 ^ q2) = Seg k ) by A4, A5, A12, A14, A22, A26, FINSEQ_1:21, FINSEQ_1:def 3;
defpred S₃[ 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 ) );
A42: for i being Nat st i in Seg k holds
ex y being set st S₃[i,y]

proof

let i be Nat; :: thesis:
assume A43: i in Seg k ; :: thesis:

now

assume A44: not f . i in dom q1 ; :: thesis:
f . i in Seg (k + 1) by A9, A38, A43, FUNCT_1:def 5;
then reconsider j = f . i as Element of NAT ;
take y = j - 1; :: thesis:
thus ( f . i in dom q1 implies y = f . i ) by A44; :: thesis:
assume not f . i in dom q1 ; :: thesis:
let t be Element of NAT ; :: thesis:
assume t = f . i ; :: thesis:
hence y = t - 1 ; :: thesis:

end;

hence ex y being set st S₃[i,y] ; :: thesis:

end;

consider g being FinSequence such that
A52: dom g = Seg k and
A53: for i being Nat st i in Seg k holds
S₃[i,g . i] from FINSEQ_1:sch 1(A42);

A54: now

let i, l be Element of NAT ; :: thesis:
assume that
A55: l = f . i and
A56: not f . i in dom q1 and
A57: i in dom g ; :: thesis:
A58: f . i in rng f by A9, A38, A52, A57, FUNCT_1:def 5;
( l < 1 or m1 < l ) by A40, A55, A56, FINSEQ_1:3;
then A59: m1 + 1 <= l by A8, A55, A58, FINSEQ_1:3, NAT_1:13;

now

assume m1 + 1 = l ; :: thesis:
then k + 1 = i by A7, A9, A12, A38, A52, A55, A57, FUNCT_1:def 8;
then k + 1 <= k + 0 by A52, A57, FINSEQ_1:3;
hence contradiction by XREAL_1:8; :: thesis:

end;

then m1 + 1 < l by A59, XXREAL_0:1;
then (m1 + 1) + 1 <= l by NAT_1:13;
hence m1 + 2 <= l ; :: thesis:

end;

A60: rng g c= dom p

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng g ; :: thesis:
then consider x being set such that
A61: x in dom g and
A62: g . x = y by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A52, A61;

now

per cases ;

suppose A63: f . x in dom q1 ; :: thesis:

then A64: f . x = g . x by A52, A53, A61;
dom q1 c= dom p by A37, A40, A41, FINSEQ_1:7;
hence y in dom p by A62, A63, A64; :: thesis:

end;

suppose A65: not f . x in dom q1 ; :: thesis:

reconsider j = f . x as Element of NAT by A9, A38, A39, A52, A61;
( j < 1 or m1 < j ) by A40, A65, FINSEQ_1:3;
then A66: ( ( j = 0 or m1 < j ) & f . x in Seg (k + 1) ) by A9, A38, A52, A61, FUNCT_1:def 5, NAT_1:14;
then reconsider l = j - 1 as Element of NAT by FINSEQ_1:3, NAT_1:20;
A67: g . x = j - 1 by A52, A53, A61, A65;
m1 + 2 <= j by A54, A61, A65;
then (m1 + 2) - 1 <= l by XREAL_1:11;
then ( m1 + 1 <= l & 1 <= m1 + 1 ) by NAT_1:12;
then A68: 1 <= l by XXREAL_0:2;
j <= k + 1 by A66, FINSEQ_1:3;
then l <= (k + 1) - 1 by XREAL_1:11;
hence y in dom p by A41, A62, A67, A68, FINSEQ_1:3; :: thesis:

end;

hence y in dom p ; :: thesis:

end;

( dom p = {} implies dom p = {} ) ;
then reconsider g = g as Function of dom (q1 ^ q2), dom (q1 ^ q2) by A41, A52, A60, FUNCT_2:def 1, RELSET_1:11;
A69: rng g = dom (q1 ^ q2)

proof

thus rng g c= dom (q1 ^ q2) ; :: according to XBOOLE_0:def 10 :: thesis:
let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A70: y in dom (q1 ^ q2) ; :: thesis:
then consider x being set such that
A71: x in dom f and
A72: f . x = y by A9, A38, A41, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A9, A71;
reconsider j = y as Element of NAT by A70;

now

per cases ;

suppose A73: x in dom g ; :: thesis:

now

per cases ;

suppose f . x in dom q1 ; :: thesis:

then g . x = f . x by A52, A53, A73;
hence y in rng g by A72, A73, FUNCT_1:def 5; :: thesis:

end;

suppose A74: not f . x in dom q1 ; :: thesis:

j <= k by A41, A70, FINSEQ_1:3;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:9;
then j + 1 in rng f by A9, FINSEQ_1:3;
then consider x1 being set such that
A75: x1 in dom f and
A76: f . x1 = j + 1 by FUNCT_1:def 5;

A77: now

assume not x1 in dom g ; :: thesis:
then x1 in (Seg (k + 1)) \ (Seg k) by A8, A52, A75, XBOOLE_0:def 5;
then x1 in {(k + 1)} by FINSEQ_3:16;
then j + 1 = m1 + 1 by A12, A76, TARSKI:def 1;
then ( 1 <= j & j <= m1 ) by A41, A70, FINSEQ_1:3;
hence contradiction by A40, A72, A74, FINSEQ_1:3; :: thesis:

end;

( j < 1 or m1 < j ) by A40, A72, A74, FINSEQ_1:3;
then not j + 1 <= m1 by A41, A70, FINSEQ_1:3, NAT_1:13;
then ( not f . x1 in dom q1 & x1 is Element of NAT ) by A9, A40, A75, A76, FINSEQ_1:3;
then g . x1 = (j + 1) - 1 by A52, A53, A76, A77
.= y ;
hence y in rng g by A77, FUNCT_1:def 5; :: thesis:

end;

hence y in rng g ; :: thesis:

end;

suppose not x in dom g ; :: thesis:

then x in (Seg (k + 1)) \ (Seg k) by A8, A52, A71, XBOOLE_0:def 5;
then x in {(k + 1)} by FINSEQ_3:16;
then A78: x = k + 1 by TARSKI:def 1;
j <= k by A41, A70, FINSEQ_1:3;
then ( 1 <= j + 1 & j + 1 <= k + 1 ) by NAT_1:12, XREAL_1:9;
then j + 1 in rng f by A9, FINSEQ_1:3;
then consider x1 being set such that
A79: x1 in dom f and
A80: f . x1 = j + 1 by FUNCT_1:def 5;

A81: now

assume not x1 in dom g ; :: thesis:
then x1 in (Seg (k + 1)) \ (Seg k) by A8, A52, A79, XBOOLE_0:def 5;
then x1 in {(k + 1)} by FINSEQ_3:16;
then j + 1 = j + 0 by A72, A78, A80, TARSKI:def 1;
hence contradiction ; :: thesis:

end;

m1 <= j by A12, A72, A78, XREAL_1:31;
then not j + 1 <= m1 by NAT_1:13;
then ( not f . x1 in dom q1 & x1 is Element of NAT ) by A9, A40, A79, A80, FINSEQ_1:3;
then g . x1 = (j + 1) - 1 by A52, A53, A80, A81
.= y ;
hence y in rng g by A81, FUNCT_1:def 5; :: thesis:

end;

hence y in rng g ; :: thesis:

end;

g is one-to-one

proof

let y1 be set ; :: according to FUNCT_1:def 8 :: thesis:
let y2 be set ; :: thesis:
assume that
A82: ( y1 in dom g & y2 in dom g ) and
A83: g . y1 = g . y2 ; :: thesis:
reconsider j1 = y1, j2 = y2 as Element of NAT by A52, A82;
A84: ( f . y1 in Seg (k + 1) & f . y2 in Seg (k + 1) ) by A9, A38, A52, A82, FUNCT_1:def 5;
then reconsider a = f . y1, b = f . y2 as Element of NAT ;

now

per cases ;

suppose ( f . y1 in dom q1 & f . y2 in dom q1 ) ; :: thesis:

then ( g . j1 = f . y1 & g . j2 = f . y2 ) by A52, A53, A82;
hence y1 = y2 by A9, A38, A52, A82, A83, FUNCT_1:def 8; :: thesis:

end;

suppose A85: ( f . y1 in dom q1 & not f . y2 in dom q1 ) ; :: thesis:

then A86: ( g . j1 = a & g . j2 = b - 1 ) by A52, A53, A82;
( a <= m1 & 1 <= b ) by A40, A84, A85, FINSEQ_1:3;
then ( (b - 1) + 1 <= m1 + 1 & 1 <= b ) by A83, A86, XREAL_1:8;
then ( b in Seg (m1 + 1) & not b in Seg m1 ) by A4, A24, A85, FINSEQ_1:3, FINSEQ_1:21;
then b in (Seg (m1 + 1)) \ (Seg m1) by XBOOLE_0:def 5;
then b in {(m1 + 1)} by FINSEQ_3:16;
then b = m1 + 1 by TARSKI:def 1;
then y2 = k + 1 by A7, A9, A12, A38, A52, A82, FUNCT_1:def 8;
hence y1 = y2 by A52, A82, FINSEQ_3:9; :: thesis:

end;

suppose A87: ( not f . y1 in dom q1 & f . y2 in dom q1 ) ; :: thesis:

then A88: ( g . j1 = a - 1 & g . j2 = b ) by A52, A53, A82;
( b <= m1 & 1 <= a ) by A40, A84, A87, FINSEQ_1:3;
then ( (a - 1) + 1 <= m1 + 1 & 1 <= a ) by A83, A88, XREAL_1:8;
then ( a in Seg (m1 + 1) & not a in Seg m1 ) by A4, A24, A87, FINSEQ_1:3, FINSEQ_1:21;
then a in (Seg (m1 + 1)) \ (Seg m1) by XBOOLE_0:def 5;
then a in {(m1 + 1)} by FINSEQ_3:16;
then a = m1 + 1 by TARSKI:def 1;
then y1 = k + 1 by A7, A9, A12, A38, A52, A82, FUNCT_1:def 8;
hence y1 = y2 by A52, A82, FINSEQ_3:9; :: thesis:

end;

suppose ( not f . y1 in dom q1 & not f . y2 in dom q1 ) ; :: thesis:

then ( g . j1 = a - 1 & g . j2 = b - 1 ) by A52, A53, A82;
then ( g . j1 = a + (- 1) & g . y2 = b + (- 1) ) ;
then a = b by A83, XCMPLX_1:2;
hence y1 = y2 by A9, A38, A52, A82, FUNCT_1:def 8; :: thesis:

end;

hence y1 = y2 ; :: thesis:

end;

then reconsider g = g as Permutation of dom (q1 ^ q2) by A69, FUNCT_2:83;

now

let i be Element of NAT ; :: thesis:
assume A89: i in dom p ; :: thesis:
then f . i in rng f by A9, A38, A41, FUNCT_1:def 5;
then reconsider j = f . i as Element of NAT by A9;

now

per cases ;

suppose f . i in dom q1 ; :: thesis:

then ( f . i = g . i & H2 . i = p . i & H1 . j = q1 . j & H2 . i = H1 . (f . i) & q1 . j = (q1 ^ q2) . j ) by A6, A8, A38, A41, A53, A89, FINSEQ_1:def 7, FUNCT_1:70;
hence p . i = (q1 ^ q2) . (g . i) ; :: thesis:

end;

suppose A90: not f . i in dom q1 ; :: thesis:

then A91: ( g . i = j - 1 & H2 . i = p . i & H2 . i = H1 . (f . i) ) by A6, A8, A38, A41, A53, A89, FUNCT_1:70;
then A92: j - 1 in dom (q1 ^ q2) by A41, A52, A69, A89, FUNCT_1:def 5;
m1 + 2 <= j by A41, A52, A54, A89, A90;
then (m1 + 2) - 1 <= j - 1 by XREAL_1:11;
then ( m1 < m1 + 1 & m1 + 1 <= j - 1 ) by XREAL_1:31;
then A93: ( m1 < j - 1 & j - 1 < j ) by XREAL_1:148, XXREAL_0:2;
then m1 < j by XXREAL_0:2;
then reconsider j1 = j - 1 as Element of NAT by NAT_1:20;
not j1 in dom q1 by A40, A93, FINSEQ_1:3;
then consider a being Nat such that
A94: a in dom q2 and
A95: j1 = (len q1) + a by A92, FINSEQ_1:38;
A96: ( H1 = q1 ^ (<*v*> ^ q2) & j in dom H1 ) by A8, A9, A36, A38, A41, A89, FINSEQ_1:45, FUNCT_1:def 5;
then consider b being Nat such that
A97: b in dom (<*v*> ^ q2) and
A98: j = (len q1) + b by A90, FINSEQ_1:38;
A99: ( (q1 ^ q2) . (j - 1) = q2 . a & H1 . j = (<*v*> ^ q2) . b ) by A94, A95, A96, A97, A98, FINSEQ_1:def 7;
A100: b = 1 + a by A95, A98;
len <*v*> = 1 by FINSEQ_1:56;
hence p . i = (q1 ^ q2) . (g . i) by A91, A94, A99, A100, FINSEQ_1:def 7; :: thesis:

end;

hence p . i = (q1 ^ q2) . (g . i) ; :: thesis:

end;

then A101: Sum p = Sum (q1 ^ q2) by A3, A12, A14, A23, A26;
( dom p = Seg (len p) & dom H1 = Seg (len H1) & dom H2 = Seg (len H2) ) by FINSEQ_1:def 3;
then Sum H2 = (Sum (q1 ^ q2)) + (Sum <*v*>) by A4, A5, A23, A101, RLVECT_1:55, RLVECT_1:61
.= ((Sum q1) + (Sum q2)) + (Sum <*v*>) by RLVECT_1:58
.= (Sum q1) + ((Sum <*v*>) + (Sum q2)) by RLVECT_1:def 6
.= (Sum q1) + (Sum (<*v*> ^ q2)) by RLVECT_1:58
.= Sum (q1 ^ (<*v*> ^ q2)) by RLVECT_1:58
.= Sum H1 by A36, FINSEQ_1:45 ;
hence Sum H1 = Sum H2 ; :: thesis:

end;

hence for k being Element of NAT st S₁[k] holds
S₁[k + 1] ; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
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 ) ; :: thesis: