let f be S-Sequence_in_R2; :: thesis: for p being Point of (TOP-REAL 2) st p in rng f holds
R_Cut (f,p) = mid (f,1,(p .. f))
let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f implies R_Cut (f,p) = mid (f,1,(p .. f)) )
assume A1: p in rng f ; :: thesis: R_Cut (f,p) = mid (f,1,(p .. f))
then consider i being Nat such that
A2: i in dom f and
A3: f . i = p by FINSEQ_2:10;
reconsider i = i as Nat ;
A4: i <= len f by A2, FINSEQ_3:25;
len f >= 2 by TOPREAL1:def 8;
then A5: rng f c= L~ f by SPPOL_2:18;
then A6: 1 <= Index (p,f) by A1, JORDAN3:8;
A7: Index (p,f) < len f by A1, A5, JORDAN3:8;
A8: 0 + 1 <= i by A2, FINSEQ_3:25;
then A9: i - 1 >= 0 by XREAL_1:19;
per cases ( 1 < i or 1 = i ) by A8, XXREAL_0:1;
suppose A10: 1 < i ; :: thesis: R_Cut (f,p) = mid (f,1,(p .. f))
1 <= len f by A8, A4, XXREAL_0:2;
then 1 in dom f by FINSEQ_3:25;
then p <> f . 1 by A2, A3, A10, FUNCT_1:def 4;
then A11: R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*> by JORDAN3:def 4;
A12: (Index (p,f)) + 1 = i by A3, A4, A10, JORDAN3:12;
A13: len (mid (f,1,(Index (p,f)))) = ((Index (p,f)) -' 1) + 1 by A6, A7, JORDAN4:8
.= i -' 1 by A1, A5, A12, JORDAN3:8, NAT_D:38 ;
A14: len (mid (f,1,i)) = (i -' 1) + 1 by A8, A4, JORDAN4:8
.= i by A8, XREAL_1:235 ;
then A15: dom (mid (f,1,i)) = Seg i by FINSEQ_1:def 3;
A16: now :: thesis: for j being Nat st j in dom (mid (f,1,i)) holds
(mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j
let j be Nat; :: thesis: ( j in dom (mid (f,1,i)) implies (mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j )
reconsider a = j as Nat ;
assume A17: j in dom (mid (f,1,i)) ; :: thesis: (mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j
then A18: 1 <= j by A15, FINSEQ_1:1;
A19: j <= i by A15, A17, FINSEQ_1:1;
now :: thesis: (mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j
per cases ( j < i or j = i ) by A19, XXREAL_0:1;
suppose j < i ; :: thesis: (mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j
then A20: j <= Index (p,f) by A12, NAT_1:13;
then j <= i -' 1 by A9, A12, XREAL_0:def 2;
then A21: j in dom (mid (f,1,(Index (p,f)))) by A13, A18, FINSEQ_3:25;
thus (mid (f,1,i)) . j = f . a by A4, A18, A19, FINSEQ_6:123
.= (mid (f,1,(Index (p,f)))) . a by A7, A18, A20, FINSEQ_6:123
.= ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j by A21, FINSEQ_1:def 7 ; :: thesis: verum
end;
suppose A22: j = i ; :: thesis: (mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j
A23: (i -' 1) + 1 = i by A8, XREAL_1:235;
thus (mid (f,1,i)) . j = f . a by A4, A18, A19, FINSEQ_6:123
.= ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j by A3, A13, A22, A23, FINSEQ_1:42 ; :: thesis: verum
end;
end;
end;
hence (mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j ; :: thesis: verum
end;
len ((mid (f,1,(Index (p,f)))) ^ <*p*>) = (i -' 1) + 1 by A13, FINSEQ_2:16
.= i by A8, XREAL_1:235 ;
then mid (f,1,i) = R_Cut (f,p) by A11, A14, A16, FINSEQ_2:9;
hence R_Cut (f,p) = mid (f,1,(p .. f)) by A2, A3, FINSEQ_5:11; :: thesis: verum
end;
suppose A24: 1 = i ; :: thesis: R_Cut (f,p) = mid (f,1,(p .. f))
then A25: R_Cut (f,p) = <*p*> by A3, JORDAN3:def 4;
A26: p = f /. 1 by A2, A3, A24, PARTFUN1:def 6;
then S: p .. f = 1 by FINSEQ_6:43;
f /. 1 = f . 1 by A2, PARTFUN1:def 6, A24;
hence R_Cut (f,p) = mid (f,1,(p .. f)) by A2, A24, A25, A26, S, JORDAN4:15; :: thesis: verum
end;
end;