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: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)} ; :: thesis: <*p*> ^ g is unfolded
let i be Nat; :: according to TOPREAL1:def 6 :: 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 :: thesis: not len g = 0
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: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; :: 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: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 ;
:: thesis: verum
end;
end;