N-min (L~ g) in rng g by SPRECT_2:43;
then consider i being Element of NAT such that
A7: ( 1 <= i & i + 1 <= len g & g . i = N-min (L~ g) ) by Th5;
thus ex b₁ being Element of NAT st
( 1 <= b₁ & b₁ + 1 <= len g & g . b₁ = N-min (L~ g) ) by A7; :: thesis: verum