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

assume for p being Real st p in X holds
p <= q ; :: thesis: ((GoB h) * ((len (GoB h)),1)) `1 <= q
hence ((GoB h) * ((len (GoB h)),1)) `1 <= q by A6, A8; :: thesis: verum
end;
hence upper_bound X = ((GoB h) * ((len (GoB h)),1)) `1 by ; :: thesis: verum
end;
hence E-bound (L~ h) = ((GoB h) * ((len (GoB h)),1)) `1 by Th17; :: thesis: verum