:: deftheorem Def6 defines lastrng FUNCT_7:def 7 :
for F being FinSequence
for b₂ being set holds
( ( F is empty implies ( b₂ = lastrng F iff b₂ is empty ) ) & ( not F is empty implies ( b₂ = lastrng F iff b₂ = proj2 (F . (len F)) ) ) );