let f1, f2 be FinSequence of (TOP-REAL 2); for n, m being Nat st len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n holds
LSeg ((f1 ^ f2),n) = LSeg (f2,m)
let n, m be Nat; ( len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n implies LSeg ((f1 ^ f2),n) = LSeg (f2,m) )
set f = f1 ^ f2;
assume that
A1:
len f1 < n
and
A2:
n + 1 <= len (f1 ^ f2)
and
A3:
m + (len f1) = n
; LSeg ((f1 ^ f2),n) = LSeg (f2,m)
A4:
1 <= m
by A1, A3, NAT_1:19;
reconsider p = (f1 ^ f2) /. n, q = (f1 ^ f2) /. (n + 1) as Point of (TOP-REAL 2) ;
A5:
n + 1 = (m + 1) + (len f1)
by A3;
len (f1 ^ f2) = (len f1) + (len f2)
by FINSEQ_1:22;
then A6:
m + 1 <= len f2
by A2, A5, XREAL_1:6;
then A7:
(f1 ^ f2) /. (n + 1) = f2 /. (m + 1)
by A5, NAT_1:11, SEQ_4:136;
m <= m + 1
by NAT_1:11;
then
m <= len f2
by A6, XXREAL_0:2;
then A8:
(f1 ^ f2) /. n = f2 /. m
by A3, A4, SEQ_4:136;
0 + 1 <= n
by A1, NAT_1:13;
hence LSeg ((f1 ^ f2),n) =
LSeg (p,q)
by A2, TOPREAL1:def 3
.=
LSeg (f2,m)
by A4, A6, A8, A7, TOPREAL1:def 3
;
verum