let f, g be FinSequence; :: thesis: for m, n, j being Nat st f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Nat st 1 <= i & i <= m holds

f . i = g . i ) & ( for i being Nat st n < i & i <= len f holds

f . i = g . i ) & m < j & j <= n holds

ex k being Nat st

( m < k & k <= n & f . j = g . k )

let m, n, j be Nat; :: thesis: ( f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Nat st 1 <= i & i <= m holds

f . i = g . i ) & ( for i being Nat st n < i & i <= len f holds

f . i = g . i ) & m < j & j <= n implies ex k being Nat st

( m < k & k <= n & f . j = g . k ) )

assume A1: f,g are_fiberwise_equipotent ; :: thesis: ( not m <= n or not n <= len f or ex i being Nat st

( 1 <= i & i <= m & not f . i = g . i ) or ex i being Nat st

( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Nat st

( m < k & k <= n & f . j = g . k ) )

assume that

A2: m <= n and

A3: n <= len f ; :: thesis: ( ex i being Nat st

( 1 <= i & i <= m & not f . i = g . i ) or ex i being Nat st

( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Nat st

( m < k & k <= n & f . j = g . k ) )

assume A4: for i being Nat st 1 <= i & i <= m holds

f . i = g . i ; :: thesis: ( ex i being Nat st

( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Nat st

( m < k & k <= n & f . j = g . k ) )

reconsider m3 = (len f) - n as Element of NAT by A3, INT_1:3, XREAL_1:48;

len g = n + m3 by A1, Th3;

then consider s2, r2 being FinSequence such that

A5: len s2 = n and

A6: len r2 = m3 and

A7: g = s2 ^ r2 by FINSEQ_2:22;

A8: len f = n + m3 ;

then consider s1, r1 being FinSequence such that

A9: len s1 = n and

A10: len r1 = m3 and

A11: f = s1 ^ r1 by FINSEQ_2:22;

A12: dom r1 = Seg m3 by A10, FINSEQ_1:def 3;

assume A13: for i being Nat st n < i & i <= len f holds

f . i = g . i ; :: thesis: ( not m < j or not j <= n or ex k being Nat st

( m < k & k <= n & f . j = g . k ) )

then A19: s1,s2 are_fiberwise_equipotent by A1, A11, A7, Th1;

reconsider m2 = n - m as Element of NAT by A2, INT_1:3, XREAL_1:48;

A20: m + 1 > m by XREAL_1:29;

len s2 = m + m2 by A5;

then consider p2, q2 being FinSequence such that

A21: len p2 = m and

A22: len q2 = m2 and

A23: s2 = p2 ^ q2 by FINSEQ_2:22;

A24: Seg m = dom p2 by A21, FINSEQ_1:def 3;

len s1 = m + m2 by A9;

then consider p1, q1 being FinSequence such that

A25: len p1 = m and

A26: len q1 = m2 and

A27: s1 = p1 ^ q1 by FINSEQ_2:22;

A28: f = p1 ^ (q1 ^ r1) by A11, A27, FINSEQ_1:32;

A29: dom p1 = Seg m by A25, FINSEQ_1:def 3;

A30: g = p2 ^ (q2 ^ r2) by A7, A23, FINSEQ_1:32;

then A33: q1,q2 are_fiberwise_equipotent by A27, A23, A19, Th31;

assume that

A34: m < j and

A35: j <= n ; :: thesis: ex k being Nat st

( m < k & k <= n & f . j = g . k )

j - (len p1) > 0 by A34, A25, XREAL_1:50;

then reconsider x = j - (len p1) as Element of NAT by INT_1:3;

A36: x <= n - (len p1) by A35, XREAL_1:9;

A37: Seg m2 = dom q2 by A22, FINSEQ_1:def 3;

A38: 1 + 0 <= x by A34, A25, INT_1:7, XREAL_1:50;

then x in dom q2 by A25, A37, A36, FINSEQ_1:1;

then consider y being set such that

A39: y in dom q2 and

A40: q1 . x = q2 . y by A33, Th30;

reconsider y = y as Nat by A39;

A41: (len p2) + y in dom s2 by A23, A39, FINSEQ_1:28;

reconsider k = (len p2) + y as Nat ;

take k ; :: thesis: ( m < k & k <= n & f . j = g . k )

1 <= y by A37, A39, FINSEQ_1:1;

then k >= (len p2) + 1 by XREAL_1:6;

hence m < k by A21, A20, XXREAL_0:2; :: thesis: ( k <= n & f . j = g . k )

y <= m2 by A37, A39, FINSEQ_1:1;

then k <= m2 + (len p2) by XREAL_1:6;

hence k <= n by A21; :: thesis: f . j = g . k

Seg m2 = dom q1 by A26, FINSEQ_1:def 3;

then A42: x in dom q1 by A25, A38, A36, FINSEQ_1:1;

then (len p1) + x in dom s1 by A27, FINSEQ_1:28;

hence f . j = s1 . ((len p1) + x) by A11, FINSEQ_1:def 7

.= q2 . y by A27, A40, A42, FINSEQ_1:def 7

.= s2 . ((len p2) + y) by A23, A39, FINSEQ_1:def 7

.= g . k by A7, A41, FINSEQ_1:def 7 ;

:: thesis: verum

f . i = g . i ) & ( for i being Nat st n < i & i <= len f holds

f . i = g . i ) & m < j & j <= n holds

ex k being Nat st

( m < k & k <= n & f . j = g . k )

let m, n, j be Nat; :: thesis: ( f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Nat st 1 <= i & i <= m holds

f . i = g . i ) & ( for i being Nat st n < i & i <= len f holds

f . i = g . i ) & m < j & j <= n implies ex k being Nat st

( m < k & k <= n & f . j = g . k ) )

assume A1: f,g are_fiberwise_equipotent ; :: thesis: ( not m <= n or not n <= len f or ex i being Nat st

( 1 <= i & i <= m & not f . i = g . i ) or ex i being Nat st

( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Nat st

( m < k & k <= n & f . j = g . k ) )

assume that

A2: m <= n and

A3: n <= len f ; :: thesis: ( ex i being Nat st

( 1 <= i & i <= m & not f . i = g . i ) or ex i being Nat st

( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Nat st

( m < k & k <= n & f . j = g . k ) )

assume A4: for i being Nat st 1 <= i & i <= m holds

f . i = g . i ; :: thesis: ( ex i being Nat st

( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Nat st

( m < k & k <= n & f . j = g . k ) )

reconsider m3 = (len f) - n as Element of NAT by A3, INT_1:3, XREAL_1:48;

len g = n + m3 by A1, Th3;

then consider s2, r2 being FinSequence such that

A5: len s2 = n and

A6: len r2 = m3 and

A7: g = s2 ^ r2 by FINSEQ_2:22;

A8: len f = n + m3 ;

then consider s1, r1 being FinSequence such that

A9: len s1 = n and

A10: len r1 = m3 and

A11: f = s1 ^ r1 by FINSEQ_2:22;

A12: dom r1 = Seg m3 by A10, FINSEQ_1:def 3;

assume A13: for i being Nat st n < i & i <= len f holds

f . i = g . i ; :: thesis: ( not m < j or not j <= n or ex k being Nat st

( m < k & k <= n & f . j = g . k ) )

now :: thesis: for i being Nat st i in dom r1 holds

r1 . i = r2 . i

then
r1 = r2
by A10, A6, FINSEQ_2:9;r1 . i = r2 . i

let i be Nat; :: thesis: ( i in dom r1 implies r1 . i = r2 . i )

reconsider a = i as Nat ;

A14: n < n + 1 by XREAL_1:29;

assume A15: i in dom r1 ; :: thesis: r1 . i = r2 . i

then A16: i in dom r2 by A6, A12, FINSEQ_1:def 3;

1 <= i by A12, A15, FINSEQ_1:1;

then n + 1 <= n + i by XREAL_1:6;

then A17: n < i + n by A14, XXREAL_0:2;

i <= m3 by A12, A15, FINSEQ_1:1;

then A18: (len s1) + i <= len f by A8, A9, XREAL_1:6;

thus r1 . i = f . ((len s1) + i) by A11, A15, FINSEQ_1:def 7

.= g . ((len s2) + a) by A13, A9, A5, A17, A18

.= r2 . i by A7, A16, FINSEQ_1:def 7 ; :: thesis: verum

end;reconsider a = i as Nat ;

A14: n < n + 1 by XREAL_1:29;

assume A15: i in dom r1 ; :: thesis: r1 . i = r2 . i

then A16: i in dom r2 by A6, A12, FINSEQ_1:def 3;

1 <= i by A12, A15, FINSEQ_1:1;

then n + 1 <= n + i by XREAL_1:6;

then A17: n < i + n by A14, XXREAL_0:2;

i <= m3 by A12, A15, FINSEQ_1:1;

then A18: (len s1) + i <= len f by A8, A9, XREAL_1:6;

thus r1 . i = f . ((len s1) + i) by A11, A15, FINSEQ_1:def 7

.= g . ((len s2) + a) by A13, A9, A5, A17, A18

.= r2 . i by A7, A16, FINSEQ_1:def 7 ; :: thesis: verum

then A19: s1,s2 are_fiberwise_equipotent by A1, A11, A7, Th1;

reconsider m2 = n - m as Element of NAT by A2, INT_1:3, XREAL_1:48;

A20: m + 1 > m by XREAL_1:29;

len s2 = m + m2 by A5;

then consider p2, q2 being FinSequence such that

A21: len p2 = m and

A22: len q2 = m2 and

A23: s2 = p2 ^ q2 by FINSEQ_2:22;

A24: Seg m = dom p2 by A21, FINSEQ_1:def 3;

len s1 = m + m2 by A9;

then consider p1, q1 being FinSequence such that

A25: len p1 = m and

A26: len q1 = m2 and

A27: s1 = p1 ^ q1 by FINSEQ_2:22;

A28: f = p1 ^ (q1 ^ r1) by A11, A27, FINSEQ_1:32;

A29: dom p1 = Seg m by A25, FINSEQ_1:def 3;

A30: g = p2 ^ (q2 ^ r2) by A7, A23, FINSEQ_1:32;

now :: thesis: for i being Nat st i in dom p1 holds

p1 . i = p2 . i

then
p1 = p2
by A25, A21, FINSEQ_2:9;p1 . i = p2 . i

let i be Nat; :: thesis: ( i in dom p1 implies p1 . i = p2 . i )

reconsider a = i as Nat ;

assume A31: i in dom p1 ; :: thesis: p1 . i = p2 . i

then A32: ( 1 <= i & i <= m ) by A29, FINSEQ_1:1;

thus p1 . i = f . i by A28, A31, FINSEQ_1:def 7

.= g . a by A4, A32

.= p2 . i by A30, A24, A29, A31, FINSEQ_1:def 7 ; :: thesis: verum

end;reconsider a = i as Nat ;

assume A31: i in dom p1 ; :: thesis: p1 . i = p2 . i

then A32: ( 1 <= i & i <= m ) by A29, FINSEQ_1:1;

thus p1 . i = f . i by A28, A31, FINSEQ_1:def 7

.= g . a by A4, A32

.= p2 . i by A30, A24, A29, A31, FINSEQ_1:def 7 ; :: thesis: verum

then A33: q1,q2 are_fiberwise_equipotent by A27, A23, A19, Th31;

assume that

A34: m < j and

A35: j <= n ; :: thesis: ex k being Nat st

( m < k & k <= n & f . j = g . k )

j - (len p1) > 0 by A34, A25, XREAL_1:50;

then reconsider x = j - (len p1) as Element of NAT by INT_1:3;

A36: x <= n - (len p1) by A35, XREAL_1:9;

A37: Seg m2 = dom q2 by A22, FINSEQ_1:def 3;

A38: 1 + 0 <= x by A34, A25, INT_1:7, XREAL_1:50;

then x in dom q2 by A25, A37, A36, FINSEQ_1:1;

then consider y being set such that

A39: y in dom q2 and

A40: q1 . x = q2 . y by A33, Th30;

reconsider y = y as Nat by A39;

A41: (len p2) + y in dom s2 by A23, A39, FINSEQ_1:28;

reconsider k = (len p2) + y as Nat ;

take k ; :: thesis: ( m < k & k <= n & f . j = g . k )

1 <= y by A37, A39, FINSEQ_1:1;

then k >= (len p2) + 1 by XREAL_1:6;

hence m < k by A21, A20, XXREAL_0:2; :: thesis: ( k <= n & f . j = g . k )

y <= m2 by A37, A39, FINSEQ_1:1;

then k <= m2 + (len p2) by XREAL_1:6;

hence k <= n by A21; :: thesis: f . j = g . k

Seg m2 = dom q1 by A26, FINSEQ_1:def 3;

then A42: x in dom q1 by A25, A38, A36, FINSEQ_1:1;

then (len p1) + x in dom s1 by A27, FINSEQ_1:28;

hence f . j = s1 . ((len p1) + x) by A11, FINSEQ_1:def 7

.= q2 . y by A27, A40, A42, FINSEQ_1:def 7

.= s2 . ((len p2) + y) by A23, A39, FINSEQ_1:def 7

.= g . k by A7, A41, FINSEQ_1:def 7 ;

:: thesis: verum