let C be Simple_closed_curve; :: thesis: for S being Segmentation of C
for i being Element of NAT st 1 <= i & i <= len S holds
S /. i in C
let S be Segmentation of C; :: thesis: for i being Element of NAT st 1 <= i & i <= len S holds
S /. i in C
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len S implies S /. i in C )
assume ( 1 <= i & i <= len S ) ; :: thesis: S /. i in C
then i in dom S by FINSEQ_3:27;
then A1: S /. i in rng S by PARTFUN2:4;
rng S c= C by Def3;
hence S /. i in C by A1; :: thesis: verum