let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2)
for n being Nat st f is unfolded & p in LSeg (f,n) holds
Ins (f,n,p) is unfolded
let p be Point of (TOP-REAL 2); for n being Nat st f is unfolded & p in LSeg (f,n) holds
Ins (f,n,p) is unfolded
let n be Nat; ( f is unfolded & p in LSeg (f,n) implies Ins (f,n,p) is unfolded )
assume that
A1:
f is unfolded
and
A2:
p in LSeg (f,n)
; Ins (f,n,p) is unfolded
set f1 = f | n;
set g1 = (f | n) ^ <*p*>;
set f2 = f /^ n;
A3:
n + 1 <= len f
by A2, TOPREAL1:def 3;
A4:
n <= n + 1
by NAT_1:11;
then A5:
len (f | n) = n
by A3, FINSEQ_1:59, XXREAL_0:2;
then A6:
n + 1 = len ((f | n) ^ <*p*>)
by FINSEQ_2:16;
A7:
n <= len f
by A3, A4, XXREAL_0:2;
1 <= (len f) - n
by A3, XREAL_1:19;
then A8:
1 <= len (f /^ n)
by A7, RFINSEQ:def 1;
then ZZ:
1 in dom (f /^ n)
by FINSEQ_3:25;
then A9:
f /. (n + 1) = (f /^ n) /. 1
by FINSEQ_5:27;
A10:
1 <= n
by A2, TOPREAL1:def 3;
then A11:
LSeg (f,n) = LSeg ((f /. n),(f /. (n + 1)))
by A3, TOPREAL1:def 3;
A12:
n in dom (f | n)
by A10, A5, FINSEQ_3:25;
then A13:
f /. n = (f | n) /. (len (f | n))
by A5, FINSEQ_4:70;
A14: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) =
((f | n) ^ <*p*>) /. ((len (f | n)) + 1)
by FINSEQ_2:16
.=
p
by FINSEQ_4:67
;
then A15:
(LSeg (((f | n) /. (len (f | n))),p)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) = LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1))
by A2, A11, A13, A9, TOPREAL1:5;
A16:
now (f | n) ^ <*p*> is unfolded
len (f | n) <> 0
by A2, A5, TOPREAL1:def 3;
then consider k being
Nat such that A17:
k + 1
= len (f | n)
by NAT_1:6;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
A18:
k + (1 + 1) <= len f
by A3, A5, A17;
per cases
( k <> 0 or k = 0 )
;
suppose
k <> 0
;
(f | n) ^ <*p*> is unfolded then A19:
1
<= k
by NAT_1:14;
LSeg (
(f | n),
k)
= LSeg (
f,
k)
by A17, Th3;
then A20:
(LSeg ((f | n),k)) /\ (LSeg (f,n)) = {(f /. n)}
by A1, A5, A17, A18, A19;
now for x being object holds
( ( x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) implies x = f /. n ) & ( x = f /. n implies x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) ) )let x be
object ;
( ( x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) implies x = f /. n ) & ( x = f /. n implies x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) ) )hereby ( x = f /. n implies x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) )
assume A21:
x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p))
;
x = f /. nthen
x in LSeg (
((f | n) /. (len (f | n))),
p)
by XBOOLE_0:def 4;
then A22:
x in LSeg (
f,
n)
by A11, A13, A9, A15, XBOOLE_0:def 3;
x in LSeg (
(f | n),
k)
by A21, XBOOLE_0:def 4;
then
x in (LSeg ((f | n),k)) /\ (LSeg (f,n))
by A22, XBOOLE_0:def 4;
hence
x = f /. n
by A20, TARSKI:def 1;
verum
end; assume A23:
x = f /. n
;
x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p))then
x in (LSeg ((f | n),k)) /\ (LSeg (f,n))
by A20, TARSKI:def 1;
then A24:
x in LSeg (
(f | n),
k)
by XBOOLE_0:def 4;
x in LSeg (
((f | n) /. (len (f | n))),
p)
by A13, A23, RLTOPSP1:68;
hence
x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p))
by A24, XBOOLE_0:def 4;
verum end; then
(LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) = {((f | n) /. (len (f | n)))}
by A13, TARSKI:def 1;
hence
(f | n) ^ <*p*> is
unfolded
by A1, A17, Th30;
verum end; end; end;
(f | n) /. (len (f | n)) = ((f | n) ^ <*p*>) /. n
by A5, A12, FINSEQ_4:68;
then
LSeg (((f | n) ^ <*p*>),n) = LSeg (((f | n) /. (len (f | n))),(((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))))
by A10, A6, TOPREAL1:def 3;
then A25:
(LSeg (((f | n) ^ <*p*>),n)) /\ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) = {(((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)))}
by A2, A14, A11, A13, A9, TOPREAL1:8;
now ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded per cases
( len (f /^ n) = 1 or len (f /^ n) <> 1 )
;
suppose
len (f /^ n) <> 1
;
((f | n) ^ <*p*>) ^ (f /^ n) is unfolded then
len (f /^ n) > 1
by A8, XXREAL_0:1;
then A26:
1
+ 1
<= len (f /^ n)
by NAT_1:13;
then
LSeg (
(f /^ n),1)
= LSeg (
((f /^ n) /. 1),
((f /^ n) /. (1 + 1)))
by TOPREAL1:def 3;
then A27:
(f /^ n) /. 1
in LSeg (
(f /^ n),1)
by RLTOPSP1:68;
A28:
1
+ 1
<= (len f) - n
by A7, A26, RFINSEQ:def 1;
then
n + (1 + 1) <= len f
by XREAL_1:19;
then A29:
{(f /. (n + 1))} =
(LSeg (f,n)) /\ (LSeg (f,(n + 1)))
by A1, A10
.=
(LSeg (f,n)) /\ (LSeg ((f /^ n),1))
by A28, Th5
;
now for x being object holds
( ( x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) implies x = (f /^ n) /. 1 ) & ( x = (f /^ n) /. 1 implies x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) ) )let x be
object ;
( ( x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) implies x = (f /^ n) /. 1 ) & ( x = (f /^ n) /. 1 implies x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) ) )hereby ( x = (f /^ n) /. 1 implies x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) )
assume A30:
x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1))
;
x = (f /^ n) /. 1then
x in LSeg (
(((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),
((f /^ n) /. 1))
by XBOOLE_0:def 4;
then A31:
x in LSeg (
f,
n)
by A11, A13, A9, A15, XBOOLE_0:def 3;
x in LSeg (
(f /^ n),1)
by A30, XBOOLE_0:def 4;
then
x in (LSeg (f,n)) /\ (LSeg ((f /^ n),1))
by A31, XBOOLE_0:def 4;
hence
x = (f /^ n) /. 1
by A9, A29, TARSKI:def 1;
verum
end; assume A32:
x = (f /^ n) /. 1
;
x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1))then
x in LSeg (
(((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),
((f /^ n) /. 1))
by RLTOPSP1:68;
hence
x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1))
by A27, A32, XBOOLE_0:def 4;
verum end; then
(LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) = {((f /^ n) /. 1)}
by TARSKI:def 1;
hence
((f | n) ^ <*p*>) ^ (f /^ n) is
unfolded
by A1, A16, A6, A25, Th31;
verum end; end; end;
hence
Ins (f,n,p) is unfolded
by FINSEQ_5:def 4; verum