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

now :: thesis: for i being Nat st i in dom r1 holds
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;

then r1 = r2 by A10, A6, FINSEQ_2:9;
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

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;

then p1 = p2 by A25, A21, FINSEQ_2:9;
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;
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;
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