:: deftheorem Def1 defines IFXFinSequence ALGSTR_4:def 1 :
for X, x being set holds
( ( x is XFinSequence of X implies IFXFinSequence (x,X) = x ) & ( x is not XFinSequence of X implies IFXFinSequence (x,X) = <%> X ) );