defpred S₁[ Element of NAT ] means ( [(len (GoB g)),$1] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (len (GoB g)),$1 ) );
set Y = { j where j is Element of NAT : S₁[j] } ;
0 <> len (GoB g) by GOBOARD1:def 5;
then 1 <= len (GoB g) by NAT_1:14;
then consider i, j being Element of NAT such that
A43: ( i in dom g & [(len (GoB g)),j] in Indices (GoB g) & g /. i = (GoB g) * (len (GoB g)),j ) by Th9;
A44: j in { j where j is Element of NAT : S₁[j] } by A43;
A45: { j where j is Element of NAT : S₁[j] } c= Seg (width (GoB g))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { j where j is Element of NAT : S₁[j] } or y in Seg (width (GoB g)) )
assume y in { j where j is Element of NAT : S₁[j] } ; :: thesis: y in Seg (width (GoB g))
then ex j being Element of NAT st
( y = j & [(len (GoB g)),j] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (len (GoB g)),j ) ) ;
then [(len (GoB g)),y] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def 5;
hence y in Seg (width (GoB g)) by ZFMISC_1:106; :: thesis: verum

end;

{ j where j is Element of NAT : S₁[j] } is Subset of NAT from DOMAIN_1:sch 7();
then reconsider Y = { j where j is Element of NAT : S₁[j] } as non empty finite Subset of NAT by A44, A45;
reconsider i1 = max Y as Element of NAT by ORDINAL1:def 13;
i1 in Y by XXREAL_2:def 8;
then consider j being Element of NAT such that
A46: ( j = i1 & [(len (GoB g)),j] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * (len (GoB g)),j ) ) ;
consider i being Element of NAT such that
A47: ( i in dom g & g /. i = (GoB g) * (len (GoB g)),j ) by A46;
( 1 <= 1 & 1 <= len (GoB g) & 1 <= i1 & i1 <= width (GoB g) ) by A46, MATRIX_1:39;
then A48: ((GoB g) * (len (GoB g)),i1) `1 = ((GoB g) * (len (GoB g)),1) `1 by GOBOARD5:3;
then A49: ((GoB g) * (len (GoB g)),i1) `1 = E-bound (L~ g) by Th41;
{ (q `2 ) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } c= REAL

proof

let X be set ; :: according to TARSKI:def 3 :: thesis: ( not X in { (q `2 ) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } or X in REAL )
assume X in { (q `2 ) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } ; :: thesis: X in REAL
then ex q being Point of (TOP-REAL 2) st
( X = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
hence X in REAL ; :: thesis: verum

end;

then reconsider B = { (q `2 ) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } as Subset of REAL ;
set s1 = ((GoB g) * (len (GoB g)),(width (GoB g))) `2 ;
for r being real number st r in B holds
((GoB g) * (len (GoB g)),(width (GoB g))) `2 >= r

proof

let r be real number ; :: thesis: ( r in B implies ((GoB g) * (len (GoB g)),(width (GoB g))) `2 >= r )
assume r in B ; :: thesis: ((GoB g) * (len (GoB g)),(width (GoB g))) `2 >= r
then consider q being Point of (TOP-REAL 2) such that
A50: ( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
1 <= len (GoB g) by GOBOARD7:34;
hence ((GoB g) * (len (GoB g)),(width (GoB g))) `2 >= r by A50, Th36; :: thesis: verum

end;

then A51: B is bounded_above by SEQ_4:def 1;
A52: ( 1 <= i & i <= len g ) by A47, FINSEQ_3:27;

now

per cases ( i < len g or i = len g ) by A52, XXREAL_0:1;

case i < len g ; :: thesis: (GoB g) * (len (GoB g)),i1 in L~ g

then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg g,i by A52, TOPREAL1:27;
hence (GoB g) * (len (GoB g)),i1 in L~ g by A46, A47, SPPOL_2:17; :: thesis: verum

end;

case i = len g ; :: thesis: (GoB g) * (len (GoB g)),i1 in L~ g

then g /. i in LSeg g,(i -' 1) by Lm9, Th3;
hence (GoB g) * (len (GoB g)),i1 in L~ g by A46, A47, SPPOL_2:17; :: thesis: verum

end;

end;

end;

then ( ((GoB g) * (len (GoB g)),i1) `1 = E-bound (L~ g) & (GoB g) * (len (GoB g)),i1 in L~ g ) by A48, Th41;
then A53: ((GoB g) * (len (GoB g)),i1) `2 in { (q `2 ) where q is Point of (TOP-REAL 2) : ( q `1 = E-bound (L~ g) & q in L~ g ) } ;
then A54: upper_bound B >= ((GoB g) * (len (GoB g)),i1) `2 by A51, SEQ_4:def 4;
for r being real number st r in B holds
r <= ((GoB g) * (len (GoB g)),i1) `2

proof

let r be real number ; :: thesis: ( r in B implies r <= ((GoB g) * (len (GoB g)),i1) `2 )
assume r in B ; :: thesis: r <= ((GoB g) * (len (GoB g)),i1) `2
then consider q being Point of (TOP-REAL 2) such that
A55: ( r = q `2 & q `1 = E-bound (L~ g) & q in L~ g ) ;
thus r <= ((GoB g) * (len (GoB g)),i1) `2 by A55, Lm4; :: thesis: verum

end;

then upper_bound B <= ((GoB g) * (len (GoB g)),i1) `2 by A53, SEQ_4:62;
then ((GoB g) * (len (GoB g)),i1) `2 = upper_bound B by A54, XXREAL_0:1
.= sup (proj2 | (E-most (L~ g))) by Th16 ;
hence ex b₁ being Element of NAT st
( [(len (GoB g)),b₁] in Indices (GoB g) & (GoB g) * (len (GoB g)),b₁ = E-max (L~ g) ) by A46, A49, EUCLID:57; :: thesis: verum