let g be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds
<*p*> ^ g is unfolded
let p be Point of (TOP-REAL 2); ( g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} implies <*p*> ^ g is unfolded )
set f = <*p*>;
A1:
len <*p*> = 1
by FINSEQ_1:39;
A2:
<*p*> /. 1 = p
by FINSEQ_4:16;
A3:
len (<*p*> ^ g) = (len <*p*>) + (len g)
by FINSEQ_1:22;
assume that
A4:
g is unfolded
and
A5:
(LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)}
; <*p*> ^ g is unfolded
let i be Nat; TOPREAL1:def 6 ( not 1 <= i or not i + 2 <= len (<*p*> ^ g) or (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))} )
assume that
A6:
1 <= i
and
A7:
i + 2 <= len (<*p*> ^ g)
; (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))}
A8:
i + (1 + 1) = (i + 1) + 1
;
per cases
( i = len <*p*> or i <> len <*p*> )
;
suppose A9:
i = len <*p*>
;
(LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))}then A10:
LSeg (
(<*p*> ^ g),
(i + 1))
= LSeg (
g,1)
by Th7;
then
1
<= len g
by NAT_1:14;
then A12:
1
in dom g
by FINSEQ_3:25;
then
LSeg (
(<*p*> ^ g),
i)
= LSeg (
(<*p*> /. (len <*p*>)),
(g /. 1))
by A9, Th8, RELAT_1:38;
hence
(LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))}
by A1, A5, A2, A9, A12, A10, FINSEQ_4:69;
verum end; suppose A13:
i <> len <*p*>
;
(LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))}reconsider j =
i - (len <*p*>) as
Element of
NAT by A1, A6, INT_1:5;
i > len <*p*>
by A1, A6, A13, XXREAL_0:1;
then
(len <*p*>) + 1
<= i
by NAT_1:13;
then A14:
1
<= j
by XREAL_1:19;
A15:
(i + 2) - (len <*p*>) <= len g
by A7, A3, XREAL_1:20;
then A16:
j + (1 + 1) <= len g
;
j + 1
<= (j + 1) + 1
by NAT_1:11;
then
j + 1
<= len g
by A15, XXREAL_0:2;
then A17:
j + 1
in dom g
by A14, SEQ_4:134;
A18:
(len <*p*>) + (j + 1) = i + 1
;
(len <*p*>) + j = i
;
hence (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) =
(LSeg (g,j)) /\ (LSeg ((<*p*> ^ g),(i + 1)))
by A14, Th7
.=
(LSeg (g,j)) /\ (LSeg (g,(j + 1)))
by A18, Th7, NAT_1:11
.=
{(g /. (j + 1))}
by A4, A14, A16
.=
{((<*p*> ^ g) /. (i + 1))}
by A18, A17, FINSEQ_4:69
;
verum end; end;