let h be non constant standard special_circular_sequence; :: thesis: N-bound (L~ h) = ((GoB h) * (1,(width (GoB h)))) `2
set X = { (q `2) where q is Point of () : q in L~ h } ;
set A = ((GoB h) * (1,(width (GoB h)))) `2 ;
consider a being object such that
A1: a in L~ h by XBOOLE_0:def 1;
A2: { (q `2) where q is Point of () : q in L~ h } c= REAL
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { (q `2) where q is Point of () : q in L~ h } or b in REAL )
assume b in { (q `2) where q is Point of () : q in L~ h } ; :: thesis:
then ex qq being Point of () st
( b = qq `2 & qq in L~ h ) ;
hence b in REAL by XREAL_0:def 1; :: thesis: verum
end;
reconsider a = a as Point of () by A1;
a `2 in { (q `2) where q is Point of () : q in L~ h } by A1;
then reconsider X = { (q `2) where q is Point of () : q in L~ h } as non empty Subset of REAL by A2;
upper_bound X = ((GoB h) * (1,(width (GoB h)))) `2
proof
A3: 1 <= len (GoB h) by GOBOARD7:32;
A4: for p being Real st p in X holds
p <= ((GoB h) * (1,(width (GoB h)))) `2
proof
let p be Real; :: thesis: ( p in X implies p <= ((GoB h) * (1,(width (GoB h)))) `2 )
assume p in X ; :: thesis: p <= ((GoB h) * (1,(width (GoB h)))) `2
then ex s being Point of () st
( p = s `2 & s in L~ h ) ;
hence p <= ((GoB h) * (1,(width (GoB h)))) `2 by ; :: thesis: verum
end;
1 <= width (GoB h) by GOBOARD7:33;
then consider q1 being Point of () such that
A5: q1 `2 = ((GoB h) * (1,(width (GoB h)))) `2 and
A6: q1 in L~ h by ;
reconsider q11 = q1 `2 as Real ;
for q being Real st ( for p being Real st p in X holds
p <= q ) holds
((GoB h) * (1,(width (GoB h)))) `2 <= q
proof
A7: q11 in X by A6;
let q be Real; :: thesis: ( ( for p being Real st p in X holds
p <= q ) implies ((GoB h) * (1,(width (GoB h)))) `2 <= q )

assume for p being Real st p in X holds
p <= q ; :: thesis: ((GoB h) * (1,(width (GoB h)))) `2 <= q
hence ((GoB h) * (1,(width (GoB h)))) `2 <= q by A5, A7; :: thesis: verum
end;
hence upper_bound X = ((GoB h) * (1,(width (GoB h)))) `2 by ; :: thesis: verum
end;
hence N-bound (L~ h) = ((GoB h) * (1,(width (GoB h)))) `2 by Th18; :: thesis: verum