:: deftheorem Def5 defines firstdom FUNCT_7:def 6 :
for F being FinSequence
for b₂ being set holds
( ( F is empty implies ( b₂ = firstdom F iff b₂ is empty ) ) & ( not F is empty implies ( b₂ = firstdom F iff b₂ = proj1 (F . 1) ) ) );