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

now :: thesis: ( ( (h /. i) `1 <= (h /. (i + 1)) `1 & p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) or ( (h /. i) `1 > (h /. (i + 1)) `1 & p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 ) )

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

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

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

end;

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

then (h /. i) `1 >= p `1 by A6, TOPREAL1:3;
hence p `1 <= ((GoB h) * ((len (GoB h)),I)) `1 by A7, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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