let n be Element of NAT ; ( n > 0 implies FTSC1 n is filled )
set f = Nbdc1 n;
assume
n > 0
; FTSC1 n is filled
then A1:
FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #)
by Def6;
let x be Element of (FTSC1 n); FIN_TOPO:def 4 x in U_FT x
x in Seg n
by A1;
then reconsider i = x as Element of NAT ;
A2:
( 1 <= i & i <= n )
by A1, FINSEQ_1:1;
A3:
( i = 1 & i < n implies Im ((Nbdc1 n),i) = {i,n,(i + 1)} )
by A1, Def5;
A4:
( 1 < i & i < n implies Im ((Nbdc1 n),i) = {i,(i -' 1),(i + 1)} )
by A1, Def5;
A5:
( i = 1 & i = n implies Im ((Nbdc1 n),i) = {i} )
by A1, Def5;
A6:
( 1 < i & i = n implies Im ((Nbdc1 n),i) = {i,(i -' 1),1} )
by A1, Def5;