let f, g be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st g is_in_the_area_of f & p in L~ g holds
<*p*> is_in_the_area_of f
let p be Point of (TOP-REAL 2); ( g is_in_the_area_of f & p in L~ g implies <*p*> is_in_the_area_of f )
assume A1:
g is_in_the_area_of f
; ( not p in L~ g or <*p*> is_in_the_area_of f )
assume
p in L~ g
; <*p*> is_in_the_area_of f
then consider i being Nat such that
A2:
1 <= i
and
A3:
i + 1 <= len g
and
A4:
p in LSeg ((g /. i),(g /. (i + 1)))
by SPPOL_2:14;
A5:
ex r being Real st
( p = ((1 - r) * (g /. i)) + (r * (g /. (i + 1))) & 0 <= r & r <= 1 )
by A4;
i <= i + 1
by NAT_1:11;
then
i <= len g
by A3, XXREAL_0:2;
then
i in dom g
by A2, FINSEQ_3:25;
then A6:
<*(g /. i)*> is_in_the_area_of f
by A1, Th45;
1 <= i + 1
by NAT_1:11;
then
i + 1 in dom g
by A3, FINSEQ_3:25;
then
<*(g /. (i + 1))*> is_in_the_area_of f
by A1, Th45;
then
<*(g /. i),(g /. (i + 1))*> is_in_the_area_of f
by A6, Th42;
hence
<*p*> is_in_the_area_of f
by A5, Th44; verum