let M be Go-board; :: thesis: for f being S-Sequence_in_R2 st f is_sequence_on M holds
for p being Point of (TOP-REAL 2) st p in rng f holds
R_Cut (f,p) is_sequence_on M
let f be S-Sequence_in_R2; :: thesis: ( f is_sequence_on M implies for p being Point of (TOP-REAL 2) st p in rng f holds
R_Cut (f,p) is_sequence_on M )
assume A1: f is_sequence_on M ; :: thesis: for p being Point of (TOP-REAL 2) st p in rng f holds
R_Cut (f,p) is_sequence_on M
let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f implies R_Cut (f,p) is_sequence_on M )
assume p in rng f ; :: thesis: R_Cut (f,p) is_sequence_on M
then R_Cut (f,p) = mid (f,1,(p .. f)) by JORDAN1G:49;
hence R_Cut (f,p) is_sequence_on M by A1, JORDAN1H:27; :: thesis: verum