let f be FinSequence; :: thesis: ( not len f is even implies len f = (2 * (Center f)) - 1 )
assume not len f is even ; :: thesis: len f = (2 * (Center f)) - 1
then consider k being Element of NAT such that
A1: len f = (2 * k) + 1 by ABIAN:9;
A2: (2 * k) mod 2 = 0 by NAT_D:13;
thus len f = (2 * (((2 * k) div 2) + (1 div 2))) + 1 by A1, Lm2, NAT_D:18
.= (2 * ((len f) div 2)) + ((2 * 1) - 1) by A1, A2, NAT_D:19
.= (2 * (Center f)) - 1 ; :: thesis: verum