let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)
for n being Element of 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); :: thesis: for n being Element of NAT st f is unfolded & p in LSeg f,n holds
Ins f,n,p is unfolded
let n be Element of NAT ; :: thesis: ( 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 ; :: thesis: Ins f,n,p is unfolded
set f1 = f | n;
set g1 = (f | n) ^ <*p*>;
set f2 = f /^ n;
A3: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:19
.= p by FINSEQ_4:82 ;
A4: ( 1 <= n & n + 1 <= len f ) by A2, TOPREAL1:def 5;
A5: n <= n + 1 by NAT_1:11;
then A6: n <= len f by A4, XXREAL_0:2;
A7: len (f | n) = n by A4, A5, FINSEQ_1:80, XXREAL_0:2;
then A8: n in dom (f | n) by A4, FINSEQ_3:27;
1 <= (len f) - n by A4, XREAL_1:21;
then A9: 1 <= len (f /^ n) by A6, RFINSEQ:def 2;
then A10: 1 in dom (f /^ n) by FINSEQ_3:27;
A11: LSeg f,n = LSeg (f /. n),(f /. (n + 1)) by A4, TOPREAL1:def 5;
A12: f /. n = (f | n) /. (len (f | n)) by A7, A8, FINSEQ_4:85;
A13: f /. (n + 1) = (f /^ n) /. 1 by A10, FINSEQ_5:30;
then A14: (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, A3, A11, A12, TOPREAL1:11;

A15: now

len (f | n) <> 0 by A2, A7, TOPREAL1:def 5;
then consider k being Nat such that
A16: k + 1 = len (f | n) by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A17: k + (1 + 1) <= len f by A4, A7, A16;
A18: f | n is unfolded by A1;

per cases ( k <> 0 or k = 0 ) ;

suppose k <> 0 ; :: thesis: (f | n) ^ <*p*> is unfolded

then A19: 1 <= k by NAT_1:14;
LSeg (f | n),k = LSeg f,k by A16, Th3;
then A20: (LSeg (f | n),k) /\ (LSeg f,n) = {(f /. n)} by A1, A7, A16, A17, A19, TOPREAL1:def 8;

now

let x be set ; :: thesis: ( ( 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 :: thesis: ( x = f /. n implies x in (LSeg (f | n),k) /\ (LSeg ((f | n) /. (len (f | n))),p) )

assume x in (LSeg (f | n),k) /\ (LSeg ((f | n) /. (len (f | n))),p) ; :: thesis: x = f /. n
then A21: ( x in LSeg (f | n),k & x in LSeg ((f | n) /. (len (f | n))),p ) by XBOOLE_0:def 4;
then x in LSeg f,n by A11, A12, A13, A14, XBOOLE_0:def 3;
then x in (LSeg (f | n),k) /\ (LSeg f,n) by A21, XBOOLE_0:def 4;
hence x = f /. n by A20, TARSKI:def 1; :: thesis: verum

end;

assume A22: x = f /. n ; :: thesis: 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 A23: x in LSeg (f | n),k by XBOOLE_0:def 4;
x in LSeg ((f | n) /. (len (f | n))),p by A12, A22, RLTOPSP1:69;
hence x in (LSeg (f | n),k) /\ (LSeg ((f | n) /. (len (f | n))),p) by A23, XBOOLE_0:def 4; :: thesis: verum

end;

then (LSeg (f | n),k) /\ (LSeg ((f | n) /. (len (f | n))),p) = {((f | n) /. (len (f | n)))} by A12, TARSKI:def 1;
hence (f | n) ^ <*p*> is unfolded by A16, A18, Th31; :: thesis: verum

end;

suppose k = 0 ; :: thesis: (f | n) ^ <*p*> is unfolded

then len ((f | n) ^ <*p*>) = 1 + 1 by A16, FINSEQ_2:19;
hence (f | n) ^ <*p*> is unfolded by Th27; :: thesis: verum

end;

end;

end;

A24: n + 1 = len ((f | n) ^ <*p*>) by A7, FINSEQ_2:19;
(f | n) /. (len (f | n)) = ((f | n) ^ <*p*>) /. n by A7, A8, FINSEQ_4:83;
then LSeg ((f | n) ^ <*p*>),n = LSeg ((f | n) /. (len (f | n))),(((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))) by A4, A24, TOPREAL1:def 5;
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, A3, A11, A12, A13, TOPREAL1:14;

now

per cases ( len (f /^ n) = 1 or len (f /^ n) <> 1 ) ;

suppose len (f /^ n) = 1 ; :: thesis: ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded

then f /^ n = <*((f /^ n) /. 1)*> by FINSEQ_5:15;
hence ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded by A15, A24, A25, Th31; :: thesis: verum

end;

suppose len (f /^ n) <> 1 ; :: thesis: ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded

then len (f /^ n) > 1 by A9, 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 5;
then A27: (f /^ n) /. 1 in LSeg (f /^ n),1 by RLTOPSP1:69;
A28: 1 + 1 <= (len f) - n by A6, A26, RFINSEQ:def 2;
then n + (1 + 1) <= len f by XREAL_1:21;
then A29: {(f /. (n + 1))} = (LSeg f,n) /\ (LSeg f,(n + 1)) by A1, A4, TOPREAL1:def 8
.= (LSeg f,n) /\ (LSeg (f /^ n),1) by A28, Th5 ;

now

let x be set ; :: thesis: ( ( 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 :: thesis: ( x = (f /^ n) /. 1 implies x in (LSeg (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)) /\ (LSeg (f /^ n),1) )

assume x in (LSeg (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)) /\ (LSeg (f /^ n),1) ; :: thesis: x = (f /^ n) /. 1
then A30: ( x in LSeg (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1) & x in LSeg (f /^ n),1 ) by XBOOLE_0:def 4;
then x in LSeg f,n by A11, A12, A13, A14, XBOOLE_0:def 3;
then x in (LSeg f,n) /\ (LSeg (f /^ n),1) by A30, XBOOLE_0:def 4;
hence x = (f /^ n) /. 1 by A13, A29, TARSKI:def 1; :: thesis: verum

end;

assume A31: x = (f /^ n) /. 1 ; :: thesis: 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:69;
hence x in (LSeg (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)) /\ (LSeg (f /^ n),1) by A27, A31, XBOOLE_0:def 4; :: thesis: verum

end;

then A32: (LSeg (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)) /\ (LSeg (f /^ n),1) = {((f /^ n) /. 1)} by TARSKI:def 1;
f /^ n is unfolded by A1;
hence ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded by A15, A24, A25, A32, Th32; :: thesis: verum

end;

end;

end;

hence Ins f,n,p is unfolded by FINSEQ_5:def 4; :: thesis: verum