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 ;
len g = n + m3 by ;
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 ;
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 ;
1 <= i by ;
then n + 1 <= n + i by XREAL_1:6;
then A17: n < i + n by ;
i <= m3 by ;
then A18: (len s1) + i <= len f by ;
thus r1 . i = f . ((len s1) + i) by
.= g . ((len s2) + a) by A13, A9, A5, A17, A18
.= r2 . i by ; :: thesis: verum
end;
then r1 = r2 by ;
then A19: s1,s2 are_fiberwise_equipotent by A1, A11, A7, Th1;
reconsider m2 = n - m as Element of NAT by ;
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 ;
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 ;
A29: dom p1 = Seg m by ;
A30: g = p2 ^ (q2 ^ r2) by ;
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 ;
thus p1 . i = f . i by
.= g . a by
.= p2 . i by ; :: thesis: verum
end;
then p1 = p2 by ;
then A33: q1,q2 are_fiberwise_equipotent by ;
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 ;
then reconsider x = j - (len p1) as Element of NAT by INT_1:3;
A36: x <= n - (len p1) by ;
A37: Seg m2 = dom q2 by ;
A38: 1 + 0 <= x by ;
then x in dom q2 by ;
then consider y being set such that
A39: y in dom q2 and
A40: q1 . x = q2 . y by ;
reconsider y = y as Nat by A39;
A41: (len p2) + y in dom s2 by ;
reconsider k = (len p2) + y as Nat ;
take k ; :: thesis: ( m < k & k <= n & f . j = g . k )
1 <= y by ;
then k >= (len p2) + 1 by XREAL_1:6;
hence m < k by ; :: thesis: ( k <= n & f . j = g . k )
y <= m2 by ;
then k <= m2 + (len p2) by XREAL_1:6;
hence k <= n by A21; :: thesis: f . j = g . k
Seg m2 = dom q1 by ;
then A42: x in dom q1 by ;
then (len p1) + x in dom s1 by ;
hence f . j = s1 . ((len p1) + x) by
.= q2 . y by
.= s2 . ((len p2) + y) by
.= g . k by ;
:: thesis: verum