let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)
for n being Nat st p in LSeg (f,n) holds
L~ f = L~ (Ins (f,n,p))
let p be Point of (TOP-REAL 2); :: thesis: for n being Nat st p in LSeg (f,n) holds
L~ f = L~ (Ins (f,n,p))
let n be Nat; :: thesis: ( p in LSeg (f,n) implies L~ f = L~ (Ins (f,n,p)) )
set f1 = f | n;
set g1 = (f | n) ^ <*p*>;
set f2 = f /^ n;
A1: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:16
.= p by FINSEQ_4:67 ;
assume A2: p in LSeg (f,n) ; :: thesis: L~ f = L~ (Ins (f,n,p))
then A3: n + 1 <= len f by TOPREAL1:def 3;
then A4: 1 <= (len f) - n by XREAL_1:19;
A5: n <= n + 1 by NAT_1:11;
then A6: len (f | n) = n by A3, FINSEQ_1:59, XXREAL_0:2;
then A7: not f | n is empty by A2, TOPREAL1:def 3;
A8: 1 <= n by A2, TOPREAL1:def 3;
then A9: n in dom (f | n) by A6, FINSEQ_3:25;
n <= len f by A3, A5, XXREAL_0:2;
then 1 <= len (f /^ n) by A4, RFINSEQ:def 1;
then A10: 1 in dom (f /^ n) by FINSEQ_3:25;
A11: LSeg (f,n) = LSeg ((f /. n),(f /. (n + 1))) by A8, A3, TOPREAL1:def 3
.= LSeg (((f | n) /. (len (f | n))),(f /. (n + 1))) by A6, A9, FINSEQ_4:70
.= LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)) by A10, FINSEQ_5:27 ;
thus L~ (Ins (f,n,p)) = L~ (((f | n) ^ <*p*>) ^ (f /^ n)) by FINSEQ_5:def 4
.= ((L~ ((f | n) ^ <*p*>)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)))) \/ (L~ (f /^ n)) by A10, Th23, RELAT_1:38
.= (((L~ (f | n)) \/ (LSeg (((f | n) /. (len (f | n))),p))) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)))) \/ (L~ (f /^ n)) by A9, Th19, RELAT_1:38
.= ((L~ (f | n)) \/ ((LSeg (((f | n) /. (len (f | n))),p)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))))) \/ (L~ (f /^ n)) by XBOOLE_1:4
.= ((L~ (f | n)) \/ (LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)))) \/ (L~ (f /^ n)) by A2, A1, A11, TOPREAL1:5
.= L~ ((f | n) ^ (f /^ n)) by A7, A10, Th23, RELAT_1:38
.= L~ f by RFINSEQ:8 ; :: thesis: verum