let C be Simple_closed_curve; :: thesis: for S being Segmentation of C
for i being Nat st 1 <= i & i <= len S holds
S /. i in C
let S be Segmentation of C; :: thesis: for i being Nat st 1 <= i & i <= len S holds
S /. i in C
let i be Nat; :: thesis: ( 1 <= i & i <= len S implies S /. i in C )
assume that
A1: 1 <= i and
A2: i <= len S ; :: thesis: S /. i in C
i in dom S by A1, A2, FINSEQ_3:25;
then A3: S /. i in rng S by PARTFUN2:2;
rng S c= C by Def3;
hence S /. i in C by A3; :: thesis: verum