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