:: deftheorem Def8 defines FuncSequence FUNCT_7:def 9 :
for X, Y being set st ( Y is empty implies X is empty ) holds
for b₃ being FuncSequence holds
( b₃ is FuncSequence of X,Y iff ( firstdom b₃ = X & lastrng b₃ c= Y ) );