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: n + 1 <= len f by A2, TOPREAL1:def 5;
A4: n <= n + 1 by NAT_1:11;
then A5: len (f | n) = n by A3, FINSEQ_1:80, XXREAL_0:2;
then A6: n + 1 = len ((f | n) ^ <*p*>) by FINSEQ_2:19;
A7: n <= len f by A3, A4, XXREAL_0:2;
1 <= (len f) - n by A3, XREAL_1:21;
then A8: 1 <= len (f /^ n) by A7, RFINSEQ:def 2;
then 1 in dom (f /^ n) by FINSEQ_3:27;
then A9: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:30;
A10: 1 <= n by A2, TOPREAL1:def 5;
then A11: LSeg f,n = LSeg (f /. n),(f /. (n + 1)) by A3, TOPREAL1:def 5;
A12: n in dom (f | n) by A10, A5, FINSEQ_3:27;
then A13: f /. n = (f | n) /. (len (f | n)) by A5, FINSEQ_4:85;
A14: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:19
.= p by FINSEQ_4:82 ;
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:11;

A16: now

len (f | n) <> 0 by A2, A5, TOPREAL1:def 5;
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 13;
A18: k + (1 + 1) <= len f by A3, A5, A17;

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 A17, Th3;
then A20: (LSeg (f | n),k) /\ (LSeg f,n) = {(f /. n)} by A1, A5, A17, A18, 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 A21: x in (LSeg (f | n),k) /\ (LSeg ((f | n) /. (len (f | n))),p) ; :: thesis: x = f /. n
then 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; :: thesis: verum

end;

assume A23: 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 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:69;
hence x in (LSeg (f | n),k) /\ (LSeg ((f | n) /. (len (f | n))),p) by A24, 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 A13, TARSKI:def 1;
hence (f | n) ^ <*p*> is unfolded by A1, A17, Th31; :: thesis: verum

end;

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

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

end;

end;

end;

(f | n) /. (len (f | n)) = ((f | n) ^ <*p*>) /. n by A5, A12, FINSEQ_4:83;
then LSeg ((f | n) ^ <*p*>),n = LSeg ((f | n) /. (len (f | n))),(((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))) by A10, A6, 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, A14, A11, A13, A9, 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 A16, A6, A25, Th31; :: thesis: verum

end;

suppose len (f /^ n) <> 1 ; :: thesis: ((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 5;
then A27: (f /^ n) /. 1 in LSeg (f /^ n),1 by RLTOPSP1:69;
A28: 1 + 1 <= (len f) - n by A7, 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, A10, 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 A30: x in (LSeg (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)) /\ (LSeg (f /^ n),1) ; :: thesis: x = (f /^ n) /. 1
then 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; :: thesis: verum

end;

assume A32: 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, A32, XBOOLE_0:def 4; :: thesis: 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, Th32; :: thesis: verum

end;

end;

end;

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