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