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;
assume that
A2: g is unfolded and
A3: (LSeg p,(g /. 1)) /\ (LSeg g,1) = {(g /. 1)} ; :: thesis: <*p*> ^ g is unfolded
A4: <*p*> /. 1 = p by FINSEQ_4:25;
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
A5: 1 <= i and
A6: i + 2 <= len (<*p*> ^ g) ; :: thesis: (LSeg (<*p*> ^ g),i) /\ (LSeg (<*p*> ^ g),(i + 1)) = {((<*p*> ^ g) /. (i + 1))}
A7: len (<*p*> ^ g) = (len <*p*>) + (len g) by FINSEQ_1:35;
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))}

now

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

end;

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

end;

suppose i <> len <*p*> ; :: thesis: (LSeg (<*p*> ^ g),i) /\ (LSeg (<*p*> ^ g),(i + 1)) = {((<*p*> ^ g) /. (i + 1))}

then A13: i > len <*p*> by A1, A5, XXREAL_0:1;
reconsider j = i - (len <*p*>) as Element of NAT by A1, A5, INT_1:18;
A14: (len <*p*>) + j = i ;
A15: (len <*p*>) + (j + 1) = i + 1 ;
(len <*p*>) + 1 <= i by A13, NAT_1:13;
then A16: 1 <= j by XREAL_1:21;
A17: (i + 2) - (len <*p*>) <= len g by A6, A7, XREAL_1:22;
then A18: j + (1 + 1) <= len g ;
j + 1 <= (j + 1) + 1 by NAT_1:11;
then j + 1 <= len g by A17, XXREAL_0:2;
then A19: j + 1 in dom g by A16, GOBOARD2:3;
thus (LSeg (<*p*> ^ g),i) /\ (LSeg (<*p*> ^ g),(i + 1)) = (LSeg g,j) /\ (LSeg (<*p*> ^ g),(i + 1)) by A14, A16, Th7
.= (LSeg g,j) /\ (LSeg g,(j + 1)) by A15, Th7, NAT_1:11
.= {(g /. (j + 1))} by A2, A16, A18, TOPREAL1:def 8
.= {((<*p*> ^ g) /. (i + 1))} by A15, A19, FINSEQ_4:84 ; :: thesis: verum

end;

end;