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
L_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
L_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
L_Cut (f,p) is_sequence_on M
let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f implies L_Cut (f,p) is_sequence_on M )
assume p in rng f ; :: thesis: L_Cut (f,p) is_sequence_on M
then L_Cut (f,p) = mid (f,(p .. f),(len f)) by Th37;
hence L_Cut (f,p) is_sequence_on M by A1, JORDAN1H:27; :: thesis: verum