let n, i be Nat; :: thesis: ( i in Seg n & i <> 1 implies (Bin1 n) /. i = FALSE )
assume that
A1: i in Seg n and
A2: i <> 1 ; :: thesis: (Bin1 n) /. i = FALSE
thus (Bin1 n) /. i = IFEQ (i,1,TRUE,FALSE) by A1, Def1
.= FALSE by A2, FUNCOP_1:def 8 ; :: thesis: verum