let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)

for k being 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 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 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 and

A3: (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} ; :: thesis: f ^ <*p*> is unfolded

A4: len <*p*> = 1 by FINSEQ_1:39;

A5: <*p*> /. 1 = p by FINSEQ_4:16;

A6: len (f ^ <*p*>) = (len f) + (len <*p*>) by FINSEQ_1:22;

let i be Nat; :: according to TOPREAL1:def 6 :: 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

A7: 1 <= i and

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

A9: i + (1 + 1) = (i + 1) + 1 ;

for k being 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 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 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 and

A3: (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} ; :: thesis: f ^ <*p*> is unfolded

A4: len <*p*> = 1 by FINSEQ_1:39;

A5: <*p*> /. 1 = p by FINSEQ_4:16;

A6: len (f ^ <*p*>) = (len f) + (len <*p*>) by FINSEQ_1:22;

let i be Nat; :: according to TOPREAL1:def 6 :: 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

A7: 1 <= i and

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

A9: i + (1 + 1) = (i + 1) + 1 ;

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

end;

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

then A11:
i + 1 in dom f
by A7, SEQ_4:135;

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 A10, Th6, XXREAL_0:2

.= (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by A9, A10, Th6

.= {(f /. (i + 1))} by A1, A7, A10

.= {((f ^ <*p*>) /. (i + 1))} by A11, FINSEQ_4:68 ;

:: thesis: verum

end;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 A10, Th6, XXREAL_0:2

.= (LSeg (f,i)) /\ (LSeg (f,(i + 1))) by A9, A10, Th6

.= {(f /. (i + 1))} by A1, A7, A10

.= {((f ^ <*p*>) /. (i + 1))} by A11, FINSEQ_4:68 ;

:: thesis: verum

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

then A12:
len f <= i + 1
by A9, NAT_1:13;

A13: not f is empty by A4, A8, A6, A9, XREAL_1:6;

then A14: len f in dom f by FINSEQ_5:6;

i + 1 <= len f by A4, A8, A6, A9, XREAL_1:6;

then A15: i + 1 = len f by A12, XXREAL_0:1;

then A16: LSeg ((f ^ <*p*>),(i + 1)) = LSeg ((f /. (len f)),(<*p*> /. 1)) by A13, Th8;

LSeg ((f ^ <*p*>),i) = LSeg (f,k) by A2, A15, Th6;

hence (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))} by A3, A5, A15, A16, A14, FINSEQ_4:68; :: thesis: verum

end;A13: not f is empty by A4, A8, A6, A9, XREAL_1:6;

then A14: len f in dom f by FINSEQ_5:6;

i + 1 <= len f by A4, A8, A6, A9, XREAL_1:6;

then A15: i + 1 = len f by A12, XXREAL_0:1;

then A16: LSeg ((f ^ <*p*>),(i + 1)) = LSeg ((f /. (len f)),(<*p*> /. 1)) by A13, Th8;

LSeg ((f ^ <*p*>),i) = LSeg (f,k) by A2, A15, Th6;

hence (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))} by A3, A5, A15, A16, A14, FINSEQ_4:68; :: thesis: verum