let p be Point of (); :: thesis: for h being non constant standard special_circular_sequence
for I being 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 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 Nat; :: thesis: ( p in L~ h & 1 <= I & I <= len (GoB h) implies p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 )
assume that
A1: p in L~ h and
A2: 1 <= I and
A3: I <= len (GoB h) ; :: thesis: p `2 <= ((GoB h) * (I,(width (GoB h)))) `2
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 ;
i <= i + 1 by NAT_1:11;
then i <= len h by ;
then A7: ((GoB h) * (I,(width (GoB h)))) `2 >= (h /. i) `2 by A2, A3, A4, Th6;
1 <= i + 1 by NAT_1:11;
then A8: ((GoB h) * (I,(width (GoB h)))) `2 >= (h /. (i + 1)) `2 by A2, A3, A5, Th6;
now :: thesis: ( ( (h /. i) `2 <= (h /. (i + 1)) `2 & p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ) or ( (h /. i) `2 > (h /. (i + 1)) `2 & p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ) )
per cases ) `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 ;
hence p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 by ; :: 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 ;
hence p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 by ; :: thesis: verum
end;
end;
end;
hence p `2 <= ((GoB h) * (I,(width (GoB h)))) `2 ; :: thesis: verum