defpred S₁[ Element of NAT ] means ( [$1,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * $1,(width (GoB g)) ) );
set Y = { j where j is Element of NAT : S₁[j] } ;
1 <= width (GoB g) by GOBOARD7:35;
then consider i, j being Element of NAT such that
A83: ( i in dom g & [j,(width (GoB g))] in Indices (GoB g) & g /. i = (GoB g) * j,(width (GoB g)) ) by Th10;
A84: j in { j where j is Element of NAT : S₁[j] } by A83;
A85: { j where j is Element of NAT : S₁[j] } c= dom (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 dom (GoB g) )
assume y in { j where j is Element of NAT : S₁[j] } ; :: thesis: y in dom (GoB g)
then ex j being Element of NAT st
( y = j & [j,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * j,(width (GoB g)) ) ) ;
then [y,(width (GoB g))] in [:(dom (GoB g)),(Seg (width (GoB g))):] by MATRIX_1:def 5;
hence y in dom (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 A84, A85;
set i1 = min Y;
min Y in Y by XXREAL_2:def 7;
then consider j being Element of NAT such that
A86: ( j = min Y & [j,(width (GoB g))] in Indices (GoB g) & ex i being Element of NAT st
( i in dom g & g /. i = (GoB g) * j,(width (GoB g)) ) ) ;
consider i being Element of NAT such that
A87: ( i in dom g & g /. i = (GoB g) * j,(width (GoB g)) ) by A86;
( 1 <= min Y & min Y <= len (GoB g) & 1 <= 1 & 1 <= width (GoB g) ) by A86, MATRIX_1:39;
then A88: ((GoB g) * (min Y),(width (GoB g))) `2 = ((GoB g) * 1,(width (GoB g))) `2 by GOBOARD5:2;
then A89: ((GoB g) * (min Y),(width (GoB g))) `2 = N-bound (L~ g) by Th42;
{ (q `1 ) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } c= REAL

proof

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

end;

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

proof

let r be real number ; :: thesis: ( r in B implies ((GoB g) * 1,(width (GoB g))) `1 <= r )
assume r in B ; :: thesis: ((GoB g) * 1,(width (GoB g))) `1 <= r
then consider q1 being Point of (TOP-REAL 2) such that
A90: ( r = q1 `1 & q1 `2 = N-bound (L~ g) & q1 in L~ g ) ;
( 1 <= width (GoB g) & width (GoB g) <= width (GoB g) ) by GOBOARD7:35;
hence ((GoB g) * 1,(width (GoB g))) `1 <= r by A90, Th33; :: thesis: verum

end;

then A91: B is bounded_below by SEQ_4:def 2;
A92: ( 1 <= i & i <= len g ) by A87, FINSEQ_3:27;

now

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

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

then i + 1 <= len g by NAT_1:13;
then g /. i in LSeg g,i by A92, TOPREAL1:27;
hence (GoB g) * (min Y),(width (GoB g)) in L~ g by A86, A87, SPPOL_2:17; :: thesis: verum

end;

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

then g /. i in LSeg g,(i -' 1) by Lm9, Th3;
hence (GoB g) * (min Y),(width (GoB g)) in L~ g by A86, A87, SPPOL_2:17; :: thesis: verum

end;

end;

end;

then ( ((GoB g) * (min Y),(width (GoB g))) `2 = N-bound (L~ g) & (GoB g) * (min Y),(width (GoB g)) in L~ g ) by A88, Th42;
then A93: ((GoB g) * (min Y),(width (GoB g))) `1 in { (q `1 ) where q is Point of (TOP-REAL 2) : ( q `2 = N-bound (L~ g) & q in L~ g ) } ;
then A94: lower_bound B <= ((GoB g) * (min Y),(width (GoB g))) `1 by A91, SEQ_4:def 5;
for r being real number st r in B holds
r >= ((GoB g) * (min Y),(width (GoB g))) `1

proof

let r be real number ; :: thesis: ( r in B implies r >= ((GoB g) * (min Y),(width (GoB g))) `1 )
assume r in B ; :: thesis: r >= ((GoB g) * (min Y),(width (GoB g))) `1
then consider q being Point of (TOP-REAL 2) such that
A95: ( r = q `1 & q `2 = N-bound (L~ g) & q in L~ g ) ;
thus r >= ((GoB g) * (min Y),(width (GoB g))) `1 by A95, Lm6; :: thesis: verum

end;

then lower_bound B >= ((GoB g) * (min Y),(width (GoB g))) `1 by A93, SEQ_4:60;
then ((GoB g) * (min Y),(width (GoB g))) `1 = lower_bound B by A94, XXREAL_0:1
.= inf (proj1 | (N-most (L~ g))) by Th17 ;
hence ex b₁ being Element of NAT st
( [b₁,(width (GoB g))] in Indices (GoB g) & (GoB g) * b₁,(width (GoB g)) = N-min (L~ g) ) by A86, A89, EUCLID:57; :: thesis: verum