:: deftheorem defines Down AFINSQ_1:def 13 :
for D being set
for f being XFinSequence of D holds Down f = f;