let p be Point of (TOP-REAL 2); 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; 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; ( 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)
; 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;
hence
p `1 <= ((GoB h) * ((len (GoB h)),I)) `1
; verum