:: deftheorem defines Center JORDAN1A:def 1 :
for f being FinSequence holds Center f = ((len f) div 2) + 1;