let V be non empty Abelian add-associative right_zeroed addLoopStr ; :: thesis: for F, G being FinSequence of the carrier of V st rng F = rng G & F is one-to-one & G is one-to-one holds
Sum F = Sum G
let F, G be FinSequence of the carrier of V; :: thesis: ( rng F = rng G & F is one-to-one & G is one-to-one implies Sum F = Sum G )
defpred S₁[ set ] means for H, I being FinSequence of the carrier of V st len H = $1 & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I;
A1: S₁[ 0 ]

proof

now

let H, I be FinSequence of the carrier of V; :: thesis: ( len H = 0 & rng H = rng I & H is one-to-one & I is one-to-one implies Sum H = Sum I )
assume that
A2: len H = 0 and
A3: rng H = rng I and
( H is one-to-one & I is one-to-one ) ; :: thesis: Sum H = Sum I
H = {} by A2;
then rng H = {} by RELAT_1:60;
then I = {} by A3, RELAT_1:64;
then len I = 0 ;
then ( Sum H = 0. V & Sum I = 0. V ) by A2, Lm5;
hence Sum H = Sum I ; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

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

proof

now

let k be Element of NAT ; :: thesis: ( ( for H, I being FinSequence of the carrier of V st len H = k & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I ) implies for H, I being FinSequence of the carrier of V st len H = k + 1 & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I )
assume A5: for H, I being FinSequence of the carrier of V st len H = k & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I ; :: thesis: for H, I being FinSequence of the carrier of V st len H = k + 1 & rng H = rng I & H is one-to-one & I is one-to-one holds
Sum H = Sum I
let H, I be FinSequence of the carrier of V; :: thesis: ( len H = k + 1 & rng H = rng I & H is one-to-one & I is one-to-one implies Sum H = Sum I )
assume that
A6: len H = k + 1 and
A7: rng H = rng I and
A8: H is one-to-one and
A9: I is one-to-one ; :: thesis: Sum H = Sum I
A10: len H = len I by A7, A8, A9, FINSEQ_1:65;
reconsider p = H | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:23;
A11: k + 1 in Seg (k + 1) by FINSEQ_1:6;
then k + 1 in dom H by A6, FINSEQ_1:def 3;
then H . (k + 1) in rng I by A7, FUNCT_1:def 5;
then consider x being set such that
A12: x in dom I and
A13: H . (k + 1) = I . x by FUNCT_1:def 5;
A14: x in Seg (k + 1) by A6, A10, A12, FINSEQ_1:def 3;
reconsider n = x as Element of NAT by A12;
reconsider v = H . (k + 1) as Element of V by A6, A11, Th54;
A15: 1 <= n by A14, FINSEQ_1:3;
then consider m1 being Nat such that
A16: 1 + m1 = n by NAT_1:10;
A17: n <= k + 1 by A14, FINSEQ_1:3;
then consider m2 being Nat such that
A18: n + m2 = k + 1 by NAT_1:10;
reconsider m2 = m2 as Element of NAT by ORDINAL1:def 13;
reconsider q1 = I | (Seg m1) as FinSequence of the carrier of V by FINSEQ_1:23;
defpred S₂[ Nat, set ] means $2 = I . (n + $1);
A20: for j being Nat st j in Seg m2 holds
ex x being set st S₂[j,x] ;
consider q2 being FinSequence such that
A21: dom q2 = Seg m2 and
A22: for k being Nat st k in Seg m2 holds
S₂[k,q2 . k] from FINSEQ_1:sch 1(A20);
rng q2 c= the carrier of V

proof

let x be set ; :: 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 set such that
A23: y in dom q2 and
A24: x = q2 . y by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A23;
( 1 <= y & y <= n + y ) by A21, A23, FINSEQ_1:3, NAT_1:12;
then A25: 1 <= n + y by XXREAL_0:2;
y <= m2 by A21, A23, FINSEQ_1:3;
then n + y <= len I by A6, A10, A18, XREAL_1:9;
then n + y in Seg (len I) by A25, FINSEQ_1:3;
then reconsider xx = I . (n + y) as Element of V by Th54;
xx in the carrier of V ;
hence x in the carrier of V by A21, A22, A23, A24; :: thesis: verum

end;

then reconsider q2 = q2 as FinSequence of the carrier of V by FINSEQ_1:def 4;
set q = q1 ^ q2;
k <= k + 1 by NAT_1:12;
then A26: len p = k by A6, FINSEQ_1:21;
m1 <= n by A16, NAT_1:11;
then A27: m1 <= k + 1 by A17, XXREAL_0:2;
then A28: ( len q1 = m1 & len q2 = m2 ) by A6, A10, A21, FINSEQ_1:21, FINSEQ_1:def 3;
then (len (q1 ^ <*v*>)) + (len q2) = ((len q1) + (len <*v*>)) + m2 by FINSEQ_1:35
.= k + 1 by A16, A18, A28, FINSEQ_1:57 ;
then A29: dom I = Seg ((len (q1 ^ <*v*>)) + (len q2)) by A6, A10, FINSEQ_1:def 3;

A30: now

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

A33: now

assume j in Seg m1 ; :: thesis: I . j = (q1 ^ <*v*>) . j
then A34: j in dom q1 by A6, A10, A27, FINSEQ_1:21;
then q1 . j = I . j by FUNCT_1:70;
hence I . j = (q1 ^ <*v*>) . j by A34, FINSEQ_1:def 7; :: thesis: verum

end;

now

assume j in {n} ; :: thesis: (q1 ^ <*v*>) . j = I . j
then A35: 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 = I . j by A13, A16, A28, A35, FINSEQ_1:57; :: thesis: verum

end;

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

end;

now

let j be Nat; :: thesis: ( j in dom q2 implies I . ((len (q1 ^ <*v*>)) + j) = q2 . j )
assume A36: j in dom q2 ; :: thesis: I . ((len (q1 ^ <*v*>)) + j) = q2 . j
len (q1 ^ <*v*>) = m1 + (len <*v*>) by A28, FINSEQ_1:35
.= n by A16, FINSEQ_1:56 ;
hence I . ((len (q1 ^ <*v*>)) + j) = q2 . j by A21, A22, A36; :: thesis: verum

end;

then A37: I = (q1 ^ <*v*>) ^ q2 by A29, A30, FINSEQ_1:def 7;
then A38: rng I = (rng (q1 ^ <*v*>)) \/ (rng q2) by FINSEQ_1:44
.= ((rng <*v*>) \/ (rng q1)) \/ (rng q2) by FINSEQ_1:44
.= ({v} \/ (rng q1)) \/ (rng q2) by FINSEQ_1:56
.= {v} \/ ((rng q1) \/ (rng q2)) by XBOOLE_1:4
.= {v} \/ (rng (q1 ^ q2)) by FINSEQ_1:44 ;
A39: m1 < n by A16, XREAL_1:31;
{v} misses rng (q1 ^ q2)

proof

assume not {v} misses rng (q1 ^ q2) ; :: thesis: contradiction
then A40: {v} /\ (rng (q1 ^ q2)) <> {} by XBOOLE_0:def 7;
consider y being Element of {v} /\ (rng (q1 ^ q2));
y in rng (q1 ^ q2) by A40, XBOOLE_0:def 4;
then A41: y in (rng q1) \/ (rng q2) by FINSEQ_1:44;
A42: y in {v} by A40, XBOOLE_0:def 4;
then A43: y = I . n by A13, TARSKI:def 1;

A44: now

assume y in rng q1 ; :: thesis: contradiction
then consider y1 being set such that
A45: y1 in dom q1 and
A46: y = q1 . y1 by FUNCT_1:def 5;
A47: y1 in Seg m1 by A6, A10, A27, A45, FINSEQ_1:21;
reconsider y1 = y1 as Element of NAT by A45;
A48: q1 . y1 = I . y1 by A45, FUNCT_1:70;
A49: y1 <= m1 by A47, FINSEQ_1:3;
A50: y1 <> n by A39, A47, FINSEQ_1:3;
( 1 <= y1 & y1 <= k + 1 ) by A27, A47, A49, FINSEQ_1:3, XXREAL_0:2;
then y1 in Seg (k + 1) by FINSEQ_1:3;
then ( y1 in dom I & n in dom I & I . y1 = I . n ) by A6, A10, A12, A13, A42, A46, A48, FINSEQ_1:def 3, TARSKI:def 1;
hence contradiction by A9, A50, FUNCT_1:def 8; :: thesis: verum

end;

now

assume y in rng q2 ; :: thesis: contradiction
then consider y1 being set such that
A51: y1 in dom q2 and
A52: y = q2 . y1 by FUNCT_1:def 5;
reconsider y1 = y1 as Element of NAT by A51;
A53: I . n = I . (n + y1) by A21, A22, A43, A51, A52;
A54: 1 <= n + y1 by A15, NAT_1:12;
y1 <= m2 by A21, A51, FINSEQ_1:3;
then n + y1 <= k + 1 by A18, XREAL_1:9;
then n + y1 in Seg (k + 1) by A54, FINSEQ_1:3;
then ( n in dom I & n + y1 in dom I ) by A6, A10, A12, FINSEQ_1:def 3;
then A55: n = n + y1 by A9, A53, FUNCT_1:def 8;
y1 <> 0 by A21, A51, FINSEQ_1:3;
hence contradiction by A55; :: thesis: verum

end;

hence contradiction by A41, A44, XBOOLE_0:def 3; :: thesis: verum

end;

then A56: rng (q1 ^ q2) = (rng I) \ {v} by A38, XBOOLE_1:88;
A57: Seg k = (Seg (k + 1)) \ {(k + 1)} by FINSEQ_1:12;
A58: rng p = H .: (Seg k) by RELAT_1:148;
A59: Seg (k + 1) = dom H by A6, FINSEQ_1:def 3;
then A60: rng H = H .: (Seg (k + 1)) by RELAT_1:146;
H .: (Seg k) = (H .: (Seg (k + 1))) \ (Im H,(k + 1)) by A8, A57, FUNCT_1:123;
then A61: rng p = rng (q1 ^ q2) by A7, A56, A58, A59, A60, FINSEQ_1:6, FUNCT_1:117;
A62: p is one-to-one by A8, FUNCT_1:84;
A63: q1 ^ q2 is one-to-one

proof

let y1, y2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not y1 in dom (q1 ^ q2) or not y2 in dom (q1 ^ q2) or not (q1 ^ q2) . y1 = (q1 ^ q2) . y2 or y1 = y2 )
assume that
A64: y1 in dom (q1 ^ q2) and
A65: y2 in dom (q1 ^ q2) and
A66: (q1 ^ q2) . y1 = (q1 ^ q2) . y2 ; :: thesis: y1 = y2
reconsider x1 = y1, x2 = y2 as Element of NAT by A64, A65;
A67: q1 is one-to-one by A9, FUNCT_1:84;

A68: now

assume A69: ( x1 in dom q1 & x2 in dom q1 ) ; :: thesis: y1 = y2
then ( q1 . x1 = (q1 ^ q2) . x1 & q1 . x2 = (q1 ^ q2) . x2 ) by FINSEQ_1:def 7;
hence y1 = y2 by A66, A67, A69, FUNCT_1:def 8; :: thesis: verum

end;

A70: now

assume A71: x1 in dom q1 ; :: thesis: ( ex j being Nat st
( j in dom q2 & x2 = (len q1) + j ) implies y1 = y2 )
given j being Nat such that A72: j in dom q2 and
A73: x2 = (len q1) + j ; :: thesis: y1 = y2
q1 . x1 = I . x1 by A71, FUNCT_1:70;
then A74: (q1 ^ q2) . x1 = I . x1 by A71, FINSEQ_1:def 7;
q2 . j = I . (n + j) by A21, A22, A72;
then A75: I . x1 = I . (n + j) by A66, A72, A73, A74, FINSEQ_1:def 7;
x1 in Seg m1 by A6, A10, A27, A71, FINSEQ_1:21;
then A76: ( 1 <= x1 & x1 <= m1 ) by FINSEQ_1:3;
then A77: x1 <= k + 1 by A27, XXREAL_0:2;
A78: 1 <= n + j by A15, NAT_1:12;
j <= m2 by A21, A72, FINSEQ_1:3;
then n + j <= k + 1 by A18, XREAL_1:9;
then ( n + j in Seg (k + 1) & x1 in Seg (k + 1) ) by A76, A77, A78, FINSEQ_1:3;
then A79: ( x1 in dom I & n + j in dom I ) by A6, A10, FINSEQ_1:def 3;
( x1 < n & n <= n + j ) by A39, A76, NAT_1:12, XXREAL_0:2;
hence y1 = y2 by A9, A75, A79, FUNCT_1:def 8; :: thesis: verum

end;

A80: now

assume A81: x2 in dom q1 ; :: thesis: ( ex j being Nat st
( j in dom q2 & x1 = (len q1) + j ) implies y1 = y2 )
given j being Nat such that A82: j in dom q2 and
A83: x1 = (len q1) + j ; :: thesis: y1 = y2
q1 . x2 = I . x2 by A81, FUNCT_1:70;
then A84: (q1 ^ q2) . x2 = I . x2 by A81, FINSEQ_1:def 7;
q2 . j = I . (n + j) by A21, A22, A82;
then A85: I . x2 = I . (n + j) by A66, A82, A83, A84, FINSEQ_1:def 7;
x2 in Seg m1 by A6, A10, A27, A81, FINSEQ_1:21;
then A86: ( 1 <= x2 & x2 <= m1 ) by FINSEQ_1:3;
then A87: x2 <= k + 1 by A27, XXREAL_0:2;
A88: 1 <= n + j by A15, NAT_1:12;
j <= m2 by A21, A82, FINSEQ_1:3;
then n + j <= k + 1 by A18, XREAL_1:9;
then ( n + j in Seg (k + 1) & x2 in Seg (k + 1) ) by A86, A87, A88, FINSEQ_1:3;
then A89: ( x2 in dom I & n + j in dom I ) by A6, A10, FINSEQ_1:def 3;
( x2 < n & n <= n + j ) by A39, A86, NAT_1:12, XXREAL_0:2;
hence y1 = y2 by A9, A85, A89, FUNCT_1:def 8; :: thesis: verum

end;

now

given j1 being Nat such that A90: j1 in dom q2 and
A91: x1 = (len q1) + j1 ; :: thesis: ( ex j2 being Nat st
( j2 in dom q2 & x2 = (len q1) + j2 ) implies y1 = y2 )
given j2 being Nat such that A92: j2 in dom q2 and
A93: x2 = (len q1) + j2 ; :: thesis: y1 = y2
A94: ( q2 . j1 = I . (n + j1) & q2 . j2 = I . (n + j2) ) by A21, A22, A90, A92;
A95: q2 . j1 = (q1 ^ q2) . (m1 + j2) by A28, A66, A90, A91, A93, FINSEQ_1:def 7
.= q2 . j2 by A28, A92, FINSEQ_1:def 7 ;
A96: ( 1 <= n + j1 & 1 <= n + j2 ) by A15, NAT_1:12;
( j1 <= m2 & j2 <= m2 ) by A21, A90, A92, FINSEQ_1:3;
then ( n + j1 <= k + 1 & n + j2 <= k + 1 ) by A18, XREAL_1:9;
then ( n + j1 in Seg (k + 1) & n + j2 in Seg (k + 1) ) by A96, FINSEQ_1:3;
then ( n + j1 in dom I & n + j2 in dom I ) by A6, A10, FINSEQ_1:def 3;
then n + j1 = n + j2 by A9, A94, A95, FUNCT_1:def 8;
hence y1 = y2 by A91, A93; :: thesis: verum

end;

hence y1 = y2 by A64, A65, A68, A70, A80, FINSEQ_1:38; :: thesis: verum

end;

A97: len <*v*> = 1 by FINSEQ_1:56;
A98: for k being Nat st k in dom p holds
H . k = p . k by FUNCT_1:70;

now

let k be Nat; :: thesis: ( k in dom <*v*> implies H . ((len p) + k) = <*v*> . k )
assume k in dom <*v*> ; :: thesis: H . ((len p) + k) = <*v*> . k
then k in Seg 1 by FINSEQ_1:55;
then k = 1 by FINSEQ_1:4, TARSKI:def 1;
hence H . ((len p) + k) = <*v*> . k by A26, FINSEQ_1:57; :: thesis: verum

end;

then H = p ^ <*v*> by A26, A59, A97, A98, FINSEQ_1:def 7;
then A99: Sum H = (Sum p) + (Sum <*v*>) by Th58;
Sum I = (Sum (q1 ^ <*v*>)) + (Sum q2) by A37, Th58
.= ((Sum q1) + (Sum <*v*>)) + (Sum q2) by Th58
.= (Sum <*v*>) + ((Sum q1) + (Sum q2)) by Def6
.= (Sum (q1 ^ q2)) + (Sum <*v*>) by Th58 ;
hence Sum H = Sum I by A5, A26, A61, A62, A63, A99; :: thesis: verum

end;

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

end;

A100: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A4);
len F = len F ;
hence ( rng F = rng G & F is one-to-one & G is one-to-one implies Sum F = Sum G ) by A100; :: thesis: verum