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

((GoB h) * (1,I)) `1 <= p `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

((GoB h) * (1,I)) `1 <= p `1

let I be Nat; :: thesis: ( p in L~ h & 1 <= I & I <= width (GoB h) implies ((GoB h) * (1,I)) `1 <= p `1 )

assume that

A1: p in L~ h and

A2: 1 <= I and

A3: I <= width (GoB h) ; :: thesis: ((GoB h) * (1,I)) `1 <= p `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) * (1,I)) `1 <= (h /. i) `1 by A2, A3, A4, Th5;

1 <= i + 1 by NAT_1:11;

then A8: ((GoB h) * (1,I)) `1 <= (h /. (i + 1)) `1 by A2, A3, A5, Th5;

for I being Nat st p in L~ h & 1 <= I & I <= width (GoB h) holds

((GoB h) * (1,I)) `1 <= p `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

((GoB h) * (1,I)) `1 <= p `1

let I be Nat; :: thesis: ( p in L~ h & 1 <= I & I <= width (GoB h) implies ((GoB h) * (1,I)) `1 <= p `1 )

assume that

A1: p in L~ h and

A2: 1 <= I and

A3: I <= width (GoB h) ; :: thesis: ((GoB h) * (1,I)) `1 <= p `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) * (1,I)) `1 <= (h /. i) `1 by A2, A3, A4, Th5;

1 <= i + 1 by NAT_1:11;

then A8: ((GoB h) * (1,I)) `1 <= (h /. (i + 1)) `1 by A2, A3, A5, Th5;

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

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