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 S_{1}[ 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;

_{1}[k] holds

S_{1}[k + 1]
;

A112: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A112, A111);

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

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 S

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

then A111:
for k being Nat st Sfor 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 A2, FINSEQ_1:def 3;

then A5: rng f = Seg (k + 1) by FUNCT_2: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 S_{2}[ Nat, object ] 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 object st S_{2}[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

S_{2}[k,q2 . k]
from FINSEQ_1:sch 1(A15);

rng q2 c= the carrier of V

reconsider q1 = H1 | (Seg m1) as FinSequence of the carrier of V by FINSEQ_1:18;

defpred S_{3}[ 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 S_{3}[i,y]

A26: dom g = Seg k and

A27: for i being Nat st i in Seg k holds

S_{3}[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;

then A40: m1 <= k by NAT_1:11;

A41: rng g c= dom p

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;

then reconsider g = g as Function of (dom (q1 ^ q2)),(dom (q1 ^ q2)) by A28, A26, A41, FUNCT_2:2;

A54: len p = k by A2, A3, A21, FINSEQ_1:17;

A55: rng g = dom (q1 ^ q2)

H2 . i = H1 . (f . i) ; :: thesis: Sum H1 = Sum H2

then A71: H2 . (k + 1) = H1 . (f . (k + 1)) by A7, FINSEQ_1:4;

(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;

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 ; :: thesis: verum

end;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 A2, FINSEQ_1:def 3;

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

A7:
dom H2 = Seg (k + 1)
by A2, A3, FINSEQ_1:def 3;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 A5, FUNCT_1:def 3;

hence f . n is Element of NAT ; :: thesis: verum

end;assume n in dom f ; :: thesis: f . n is Element of NAT

then f . n in Seg (k + 1) by A5, FUNCT_1:def 3;

hence f . n is Element of NAT ; :: thesis: verum

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 S

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 object st S

consider q2 being FinSequence such that

A16: dom q2 = Seg m2 and

A17: for k being Nat st k in Seg m2 holds

S

rng q2 c= the carrier of V

proof

then reconsider q2 = q2 as FinSequence of the carrier of V by FINSEQ_1:def 4;
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 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; :: thesis: verum

end;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 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; :: thesis: verum

reconsider q1 = H1 | (Seg m1) as FinSequence of the carrier of V by FINSEQ_1:18;

defpred S

$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 S

proof

consider g being FinSequence such that
let i be Nat; :: thesis: ( i in Seg k implies ex y being object st S_{3}[i,y] )

assume A24: i in Seg k ; :: thesis: ex y being object st S_{3}[i,y]

_{3}[i,y]
; :: thesis: verum

end;assume A24: i in Seg k ; :: thesis: ex y being object st S

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 ) ) )

hence
ex y being object st S( ( 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 A9, A5, A22, A24, FUNCT_1:def 3;

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;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

A26: dom g = Seg k and

A27: for i being Nat st i in Seg k holds

S

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 :: thesis: for i, l being Nat st l = f . i & not f . i in dom q1 & i in dom g holds

m1 + 2 <= l

A37:
len q1 = m1
by A2, A29, FINSEQ_1:17;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 A30, A32, A33, FINSEQ_1:1;

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 ; :: thesis: verum

end;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 A30, A32, A33, FINSEQ_1:1;

A36: now :: thesis: not m1 + 1 = l

f . i in rng f
by A9, A22, A26, A34, FUNCT_1:def 3;assume
m1 + 1 = l
; :: thesis: contradiction

then k + 1 = i by A10, A9, A14, A22, A26, A32, A34, FUNCT_1:def 4;

then k + 1 <= k + 0 by A26, A34, FINSEQ_1:1;

hence contradiction by XREAL_1:6; :: thesis: verum

end;then k + 1 = i by A10, A9, A14, A22, A26, A32, A34, FUNCT_1:def 4;

then k + 1 <= k + 0 by A26, A34, FINSEQ_1:1;

hence contradiction by XREAL_1:6; :: thesis: verum

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 ; :: thesis: verum

A38: now :: thesis: for j being Nat st j in dom q2 holds

H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j

1 + k = 1 + (m1 + m2)
by A14, A13;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 + (len <*v*>) by A37, FINSEQ_1:22

.= n by A14, FINSEQ_1:39 ;

hence H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j by A16, A17, A39; :: thesis: verum

end;assume A39: j in dom q2 ; :: thesis: H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j

len (q1 ^ <*v*>) = m1 + (len <*v*>) by A37, FINSEQ_1:22

.= n by A14, FINSEQ_1:39 ;

hence H1 . ((len (q1 ^ <*v*>)) + j) = q2 . j by A16, A17, A39; :: thesis: verum

then A40: m1 <= k by NAT_1:11;

A41: rng g c= dom p

proof

set q = q1 ^ q2;
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;

end;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 pend;

hence
y in dom p
; :: thesis: verumper cases
( f . x in dom q1 or not f . x in dom q1 )
;

end;

suppose A44:
f . x in dom q1
; :: thesis: y in dom p

A45:
dom q1 c= dom p
by A40, A30, A28, FINSEQ_1:5;

f . x = g . x by A26, A27, A42, A44;

hence y in dom p by A43, A44, A45; :: thesis: verum

end;f . x = g . x by A26, A27, A42, A44;

hence y in dom p by A43, A44, A45; :: thesis: verum

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 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; :: thesis: verum

end;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; :: thesis: verum

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;

then reconsider g = g as Function of (dom (q1 ^ q2)),(dom (q1 ^ q2)) by A28, A26, A41, FUNCT_2:2;

A54: len p = k by A2, A3, A21, FINSEQ_1:17;

A55: rng g = dom (q1 ^ q2)

proof

assume A70:
for i being Nat st i in dom H2 holds
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 A5, A22, A53, A56, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A9, A57;

end;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 A5, A22, A53, A56, FUNCT_1:def 3;

reconsider x = x as Element of NAT by A9, A57;

now :: thesis: y in rng gend;

hence
y in rng g
; :: thesis: verumper cases
( x in dom g or not x in dom g )
;

end;

suppose A59:
x in dom g
; :: thesis: y in rng g

end;

now :: thesis: y in rng gend;

hence
y in rng g
; :: thesis: verumper cases
( f . x in dom q1 or not f . x in dom q1 )
;

end;

suppose A60:
not f . x in dom q1
; :: thesis: 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 object such that

A61: x1 in dom f and

A62: f . x1 = j + 1 by FUNCT_1:def 3;

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; :: thesis: verum

end;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 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

( j < 1 or m1 < j )
by A30, A58, A60, FINSEQ_1:1;assume
not x1 in dom g
; :: thesis: contradiction

then 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; :: thesis: verum

end;then 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; :: thesis: verum

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; :: thesis: verum

suppose A65:
not x in dom g
; :: thesis: 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 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 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;

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; :: thesis: verum

end;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 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 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;

A69: now :: thesis: x1 in dom g

m1 <= j
by A14, A58, A68, XREAL_1:29;assume
not x1 in dom g
; :: thesis: contradiction

then x1 in (Seg (k + 1)) \ (Seg k) by A4, A26, A66, XBOOLE_0:def 5;

then x1 in {(k + 1)} by FINSEQ_3:15;

then j + 1 = j + 0 by A58, A68, A67, TARSKI:def 1;

hence contradiction ; :: thesis: verum

end;then x1 in (Seg (k + 1)) \ (Seg k) by A4, A26, A66, XBOOLE_0:def 5;

then x1 in {(k + 1)} by FINSEQ_3:15;

then j + 1 = j + 0 by A58, A68, A67, TARSKI:def 1;

hence contradiction ; :: thesis: verum

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; :: thesis: verum

H2 . i = H1 . (f . i) ; :: thesis: Sum H1 = Sum H2

then A71: H2 . (k + 1) = H1 . (f . (k + 1)) by A7, FINSEQ_1:4;

A72: now :: thesis: for j being Nat st j in dom (q1 ^ <*v*>) holds

H1 . j = (q1 ^ <*v*>) . j

g is one-to-one
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

.= m1 + 1 by FINSEQ_1:40 ;

then j in Seg (m1 + 1) by A73, FINSEQ_1:def 3;

then j in (Seg m1) \/ {n} by A14, FINSEQ_1:9;

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

end;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 A2, A29, FINSEQ_1:17;

then q1 . j = H1 . j by FUNCT_1:47;

hence H1 . j = (q1 ^ <*v*>) . j by A75, FINSEQ_1:def 7; :: thesis: verum

end;then A75: j in dom q1 by A2, A29, FINSEQ_1:17;

then q1 . j = H1 . j by FUNCT_1:47;

hence H1 . j = (q1 ^ <*v*>) . j by A75, FINSEQ_1:def 7; :: thesis: verum

A76: now :: thesis: ( j in {n} implies (q1 ^ <*v*>) . j = H1 . j )

len (q1 ^ <*v*>) =
m1 + (len <*v*>)
by A37, FINSEQ_1:22
( 1 in Seg 1 & len <*v*> = 1 )
by FINSEQ_1:1, FINSEQ_1:39;

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 A71, A14, A37, A77, FINSEQ_1:40; :: thesis: verum

end;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 A71, A14, A37, A77, FINSEQ_1:40; :: thesis: verum

.= m1 + 1 by FINSEQ_1:40 ;

then j in Seg (m1 + 1) by A73, FINSEQ_1:def 3;

then j in (Seg m1) \/ {n} by A14, FINSEQ_1:9;

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

proof

then reconsider g = g as Permutation of (dom (q1 ^ q2)) by A55, FUNCT_2:57;
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 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;

end;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 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 :: thesis: y1 = y2end;

hence
y1 = y2
; :: thesis: verumper 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 ) )
;

end;

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 A9, A22, A26, A78, A79, A80, FUNCT_1:def 4; :: thesis: verum

end;hence y1 = y2 by A9, A22, A26, A78, A79, A80, FUNCT_1:def 4; :: thesis: verum

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

then 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; :: thesis: verum

end;( 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; :: thesis: verum

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

then 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; :: thesis: verum

end;( 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; :: thesis: verum

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

then
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; :: thesis: verum

end;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; :: thesis: verum

(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 :: thesis: for i being Nat st i in dom p holds

p . i = (q1 ^ q2) . (g . i)

then
Sum p = Sum (q1 ^ q2)
by A1, A14, A13, A54, A52;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 A9, A22, A28, FUNCT_1:def 3;

then reconsider j = f . i as Element of NAT by A5;

end;assume A94: i in dom p ; :: thesis: 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 :: thesis: p . i = (q1 ^ q2) . (g . i)end;

hence
p . i = (q1 ^ q2) . (g . i)
; :: thesis: verumper cases
( f . i in dom q1 or not f . i in dom q1 )
;

end;

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 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; :: thesis: verum

end;( 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; :: thesis: verum

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 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; :: thesis: verum

end;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; :: thesis: verum

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 ; :: thesis: verum

S

A112: S

proof

for k being Nat holds S
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 A113, RLVECT_1:75;

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 A113, A114, RLVECT_1:75; :: thesis: verum

end;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 A113, RLVECT_1:75;

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 A113, A114, RLVECT_1:75; :: thesis: verum

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