let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: for n being Nat st f is unfolded & p in LSeg (f,n) holds
Ins (f,n,p) is unfolded
let n be 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 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 :: thesis: (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 ; :: 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;

now :: thesis: 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 ; :: 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:68;
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, Th30; :: thesis: verum

end;

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

then len ((f | n) ^ <*p*>) = 1 + 1 by A17, FINSEQ_2:16;
hence (f | n) ^ <*p*> is unfolded by Th26; :: thesis: 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 :: thesis: ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded

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:14
.= <*((f /^ n) /. 1)*> by ZZ, PARTFUN1:def 6 ;
hence ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded by A16, A6, A25, Th30; :: 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 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 :: thesis: 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 ; :: 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: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; :: 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, Th31; :: thesis: verum

end;

end;

end;

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