let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)
for k being Element of NAT st f is unfolded & k + 1 = len f & (LSeg f,k) /\ (LSeg (f /. (len f)),p) = {(f /. (len f))} holds
f ^ <*p*> is unfolded
let p be Point of (TOP-REAL 2); :: thesis: for k being Element of NAT st f is unfolded & k + 1 = len f & (LSeg f,k) /\ (LSeg (f /. (len f)),p) = {(f /. (len f))} holds
f ^ <*p*> is unfolded
let k be Element of NAT ; :: thesis: ( f is unfolded & k + 1 = len f & (LSeg f,k) /\ (LSeg (f /. (len f)),p) = {(f /. (len f))} implies f ^ <*p*> is unfolded )
set g = <*p*>;
assume that
A1: f is unfolded and
A2: ( k + 1 = len f & (LSeg f,k) /\ (LSeg (f /. (len f)),p) = {(f /. (len f))} ) ; :: thesis: f ^ <*p*> is unfolded
A3: len <*p*> = 1 by FINSEQ_1:56;
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 (f ^ <*p*>) or (LSeg (f ^ <*p*>),i) /\ (LSeg (f ^ <*p*>),(i + 1)) = {((f ^ <*p*>) /. (i + 1))} )
assume that
A5: 1 <= i and
A6: i + 2 <= len (f ^ <*p*>) ; :: thesis: (LSeg (f ^ <*p*>),i) /\ (LSeg (f ^ <*p*>),(i + 1)) = {((f ^ <*p*>) /. (i + 1))}
A7: len (f ^ <*p*>) = (len f) + (len <*p*>) by FINSEQ_1:35;
A8: i + (1 + 1) = (i + 1) + 1 ;

per cases ( i + 2 <= len f or i + 2 > len f ) ;

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

then A10: i + 1 in dom f by A5, GOBOARD2:4;
i + 1 <= (i + 1) + 1 by NAT_1:11;
hence (LSeg (f ^ <*p*>),i) /\ (LSeg (f ^ <*p*>),(i + 1)) = (LSeg f,i) /\ (LSeg (f ^ <*p*>),(i + 1)) by A9, Th6, XXREAL_0:2
.= (LSeg f,i) /\ (LSeg f,(i + 1)) by A8, A9, Th6
.= {(f /. (i + 1))} by A1, A5, A9, TOPREAL1:def 8
.= {((f ^ <*p*>) /. (i + 1))} by A10, FINSEQ_4:83 ;
:: thesis: verum

end;

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

A12: i + 1 <= len f by A3, A6, A7, A8, XREAL_1:8;
then A13: not f is empty ;
len f <= i + 1 by A8, A11, NAT_1:13;
then A14: i + 1 = len f by A12, XXREAL_0:1;
then A15: LSeg (f ^ <*p*>),i = LSeg f,k by A2, Th6;
A16: LSeg (f ^ <*p*>),(i + 1) = LSeg (f /. (len f)),(<*p*> /. 1) by A13, A14, Th8;
len f in dom f by A13, FINSEQ_5:6;
hence (LSeg (f ^ <*p*>),i) /\ (LSeg (f ^ <*p*>),(i + 1)) = {((f ^ <*p*>) /. (i + 1))} by A2, A4, A14, A15, A16, FINSEQ_4:83; :: thesis: verum

end;

end;