let f, g be FinSequence; :: thesis:
let m, n, j be Element of NAT ; :: thesis:
assume A1: f,g are_fiberwise_equipotent ; :: thesis:
assume A2: ( m <= n & n <= len f ) ; :: thesis:
assume A3: for i being Element of NAT st 1 <= i & i <= m holds
f . i = g . i ; :: thesis:
assume A4: for i being Element of NAT st n < i & i <= len f holds
f . i = g . i ; :: thesis:
assume A5: ( m < j & j <= n ) ; :: thesis:
reconsider m2 = n - m as Element of NAT by A2, INT_1:16, XREAL_1:50;
reconsider m3 = (len f) - n as Element of NAT by A2, INT_1:16, XREAL_1:50;
A6: len f = n + m3 ;
A7: len g = n + m3 by A1, Th16;
consider s1, r1 being FinSequence such that
A8: ( len s1 = n & len r1 = m3 & f = s1 ^ r1 ) by A6, FINSEQ_2:25;
consider s2, r2 being FinSequence such that
A9: ( len s2 = n & len r2 = m3 & g = s2 ^ r2 ) by A7, FINSEQ_2:25;
len s1 = m + m2 by A8;
then consider p1, q1 being FinSequence such that
A10: ( len p1 = m & len q1 = m2 & s1 = p1 ^ q1 ) by FINSEQ_2:25;
len s2 = m + m2 by A9;
then consider p2, q2 being FinSequence such that
A11: ( len p2 = m & len q2 = m2 & s2 = p2 ^ q2 ) by FINSEQ_2:25;
A12: f = p1 ^ (q1 ^ r1) by A8, A10, FINSEQ_1:45;
A13: g = p2 ^ (q2 ^ r2) by A9, A11, FINSEQ_1:45;
A15: Seg m = dom p2 by A11, FINSEQ_1:def 3;
X: dom r1 = Seg m3 by A8, FINSEQ_1:def 3;

now

let i be Nat; :: thesis:
reconsider a = i as Element of NAT by ORDINAL1:def 13;
assume A16: i in dom r1 ; :: thesis:
A18: i in dom r2 by A9, A16, X, FINSEQ_1:def 3;
A19: ( 1 <= i & i <= m3 ) by A16, X, FINSEQ_1:3;
then A20: n + 1 <= n + i by XREAL_1:8;
n < n + 1 by XREAL_1:31;
then A21: n < i + n by A20, XXREAL_0:2;
A22: (len s1) + i <= len f by A6, A8, A19, XREAL_1:8;
thus r1 . i = f . ((len s1) + i) by A8, A16, FINSEQ_1:def 7
.= g . ((len s2) + a) by A4, A8, A9, A21, A22
.= r2 . i by A9, A18, FINSEQ_1:def 7 ; :: thesis:

end;

then r1 = r2 by A8, A9, FINSEQ_2:10;
then A23: s1,s2 are_fiberwise_equipotent by A1, A8, A9, Th14;
X: dom p1 = Seg m by A10, FINSEQ_1:def 3;

now

let i be Nat; :: thesis:
reconsider a = i as Element of NAT by ORDINAL1:def 13;
assume A24: i in dom p1 ; :: thesis:
then A25: ( 1 <= i & i <= m ) by X, FINSEQ_1:3;
thus p1 . i = f . i by A12, A24, FINSEQ_1:def 7
.= g . a by A3, A25
.= p2 . i by A13, A15, A24, X, FINSEQ_1:def 7 ; :: thesis:

end;

then p1 = p2 by A10, A11, FINSEQ_2:10;
then A26: q1,q2 are_fiberwise_equipotent by A10, A11, A23, Th10;
j - (len p1) > 0 by A5, A10, XREAL_1:52;
then reconsider x = j - (len p1) as Element of NAT by INT_1:16;
A27: Seg m2 = dom q1 by A10, FINSEQ_1:def 3;
A28: Seg m2 = dom q2 by A11, FINSEQ_1:def 3;
A29: 1 + 0 <= x by A5, A10, INT_1:20, XREAL_1:52;
A30: x <= n - (len p1) by A5, XREAL_1:11;
then x in dom q2 by A10, A28, A29, FINSEQ_1:3;
then consider y being set such that
A31: ( y in dom q2 & q1 . x = q2 . y ) by A26, Th9;
reconsider y = y as Element of NAT by A31;
A32: ( 1 <= y & y <= m2 ) by A28, A31, FINSEQ_1:3;
reconsider k = (len p2) + y as Element of NAT by ORDINAL1:def 13;
take k ; :: thesis:
A33: k >= (len p2) + 1 by A32, XREAL_1:8;
m + 1 > m by XREAL_1:31;
hence m < k by A11, A33, XXREAL_0:2; :: thesis:
k <= m2 + (len p2) by A32, XREAL_1:8;
hence k <= n by A11; :: thesis:
A34: x in dom q1 by A10, A27, A29, A30, FINSEQ_1:3;
then A35: (len p1) + x in dom s1 by A10, FINSEQ_1:41;
A36: (len p2) + y in dom s2 by A11, A31, FINSEQ_1:41;
thus f . j = s1 . ((len p1) + x) by A8, A35, FINSEQ_1:def 7
.= q2 . y by A10, A31, A34, FINSEQ_1:def 7
.= s2 . ((len p2) + y) by A11, A31, FINSEQ_1:def 7
.= g . k by A9, A36, FINSEQ_1:def 7 ; :: thesis: