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