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;

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;

end;

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;

.= 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;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

len ((mid (f,1,(Index (p,f)))) ^ <*p*>) =
(i -' 1) + 1
by A13, FINSEQ_2:16
(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;

end;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*>) . jend;

hence
(mid (f,1,i)) . j = ((mid (f,1,(Index (p,f)))) ^ <*p*>) . j
; :: thesis: verumper cases
( j < i or j = i )
by A19, XXREAL_0:1;

end;

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;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

.= 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

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;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