let f be FinSequence; :: thesis: ( len f is even implies len f = (2 * (Center f)) - 2 )
assume ex k being Element of NAT st len f = 2 * k ; :: according to ABIAN:def 2 :: thesis: len f = (2 * (Center f)) - 2
hence len f = ((2 * ((len f) div 2)) + (2 * 1)) - 2 by NAT_D:18
.= (2 * (Center f)) - 2 ;
:: thesis: verum