let p be Point of (TOP-REAL 2); :: thesis: for h being non constant standard special_circular_sequence
for I being Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds
p `2 <= ((GoB h) * I,(width (GoB h))) `2
let h be non constant standard special_circular_sequence; :: thesis: for I being Element of NAT st p in L~ h & 1 <= I & I <= len (GoB h) holds
p `2 <= ((GoB h) * I,(width (GoB h))) `2
let I be Element of NAT ; :: thesis: ( p in L~ h & 1 <= I & I <= len (GoB h) implies p `2 <= ((GoB h) * I,(width (GoB h))) `2 )
assume A1: ( p in L~ h & 1 <= I & I <= len (GoB h) ) ; :: thesis: p `2 <= ((GoB h) * I,(width (GoB h))) `2
then consider i being Element of NAT such that
A2: ( 1 <= i & i + 1 <= len h & p in LSeg (h /. i),(h /. (i + 1)) ) by SPPOL_2:14;
i <= i + 1 by NAT_1:11;
then A3: i <= len h by A2, XXREAL_0:2;
A4: 1 <= i + 1 by NAT_1:11;
A5: ((GoB h) * I,(width (GoB h))) `2 >= (h /. i) `2 by A1, A2, A3, Th8;
A6: ((GoB h) * I,(width (GoB h))) `2 >= (h /. (i + 1)) `2 by A1, A2, A4, Th8;

now

per cases ( (h /. i) `2 <= (h /. (i + 1)) `2 or (h /. i) `2 > (h /. (i + 1)) `2 ) ;

case (h /. i) `2 <= (h /. (i + 1)) `2 ; :: thesis: p `2 <= ((GoB h) * I,(width (GoB h))) `2

then (h /. (i + 1)) `2 >= p `2 by A2, TOPREAL1:10;
hence p `2 <= ((GoB h) * I,(width (GoB h))) `2 by A6, XXREAL_0:2; :: thesis: verum

end;

case (h /. i) `2 > (h /. (i + 1)) `2 ; :: thesis: p `2 <= ((GoB h) * I,(width (GoB h))) `2

then (h /. i) `2 >= p `2 by A2, TOPREAL1:10;
hence p `2 <= ((GoB h) * I,(width (GoB h))) `2 by A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence p `2 <= ((GoB h) * I,(width (GoB h))) `2 ; :: thesis: verum