let f1, f2 be FinSequence of (TOP-REAL 2); for n, m being Element of 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 Element of 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:35;
then A6:
m + 1 <= len f2
by A2, A5, XREAL_1:8;
then A7:
(f1 ^ f2) /. (n + 1) = f2 /. (m + 1)
by A5, NAT_1:11, SEQ_4:153;
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:153;
0 + 1 <= n
by A1, NAT_1:13;
hence LSeg (f1 ^ f2),n =
LSeg p,q
by A2, TOPREAL1:def 5
.=
LSeg f2,m
by A4, A6, A8, A7, TOPREAL1:def 5
;
verum