let g be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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:56;
A2: <*p*> /. 1 = p by FINSEQ_4:25;
A3: len (<*p*> ^ g) = (len <*p*>) + (len g) by FINSEQ_1:35;
assume that
A4: g is unfolded and
A5: (LSeg p,(g /. 1)) /\ (LSeg g,1) = {(g /. 1)} ; :: thesis: <*p*> ^ g is unfolded
let i be Nat; :: according to TOPREAL1:def 8 :: thesis: ( 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) ; :: thesis: (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*> ; :: thesis: (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;

now

i <= i + 1 by NAT_1:11;
then A11: i < i + (1 + 1) by A8, NAT_1:13;
assume len g = 0 ; :: thesis: contradiction
hence contradiction by A1, A6, A7, A3, A11, XXREAL_0:2; :: thesis: verum

end;

then 1 <= len g by NAT_1:14;
then A12: 1 in dom g by FINSEQ_3:27;
then LSeg (<*p*> ^ g),i = LSeg (<*p*> /. (len <*p*>)),(g /. 1) by A9, Th8, RELAT_1:60;
hence (LSeg (<*p*> ^ g),i) /\ (LSeg (<*p*> ^ g),(i + 1)) = {((<*p*> ^ g) /. (i + 1))} by A1, A5, A2, A9, A12, A10, FINSEQ_4:84; :: thesis: verum

end;

suppose A13: i <> len <*p*> ; :: thesis: (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:18;
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:21;
A15: (i + 2) - (len <*p*>) <= len g by A7, A3, XREAL_1:22;
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, GOBOARD2:3;
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, TOPREAL1:def 8
.= {((<*p*> ^ g) /. (i + 1))} by A18, A17, FINSEQ_4:84 ;
:: thesis: verum

end;

end;