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:57;
hence R_Cut f,p is_sequence_on M by A1, JORDAN1H:33; :: thesis: verum