let f be FinSequence of (TOP-REAL 2); 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); 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; ( 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))}
; 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; TOPREAL1:def 6 ( 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*>)
; (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 )
;
suppose A10:
i + 2
<= len f
;
(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
;
verum end; suppose
i + 2
> len f
;
(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;
verum end; end;