let f, g be FinSequence; :: thesis:
let m, n, j be Nat; :: thesis:
assume A1: f,g are_fiberwise_equipotent ; :: thesis:
assume that
A2: m <= n and
A3: n <= len f ; :: thesis:
assume A4: for i being Nat st 1 <= i & i <= m holds
f . i = g . i ; :: thesis:
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:

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;

let i be Nat; :: thesis:
reconsider a = i as Nat ;
assume A31: i in dom p1 ; :: thesis:
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:

end;