let n be Element of NAT ; :: thesis: n -BinarySequence 0 = ZERO n
A1: len (n -BinarySequence 0 ) = n by FINSEQ_1:def 18;
then A2: dom (n -BinarySequence 0 ) = Seg n by FINSEQ_1:def 3;
A3: len (ZERO n) = n by FINSEQ_1:def 18;
then A4: dom (ZERO n) = Seg n by FINSEQ_1:def 3;
A5: dom (n -BinarySequence 0 ) = Seg n by A1, FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom (n -BinarySequence 0 ) implies (n -BinarySequence 0 ) . j = (ZERO n) . j )
A6: (0 div (2 to_power (j -' 1))) mod 2 = 0 mod 2 by NAT_2:4
.= 0 by NAT_D:26 ;
assume A7: j in dom (n -BinarySequence 0 ) ; :: thesis: (n -BinarySequence 0 ) . j = (ZERO n) . j
then j in dom (ZERO n) by A2, FUNCOP_1:19;
then A8: (ZERO n) /. j = (n |-> FALSE ) . j by PARTFUN1:def 8
.= FALSE by A2, A7, FUNCOP_1:13 ;
thus (n -BinarySequence 0 ) . j = (n -BinarySequence 0 ) /. j by A7, PARTFUN1:def 8
.= IFEQ ((0 div (2 to_power (j -' 1))) mod 2),0 ,FALSE ,TRUE by A2, A7, BINARI_3:def 1
.= (ZERO n) /. j by A6, A8, FUNCOP_1:def 8
.= (ZERO n) . j by A5, A4, A7, PARTFUN1:def 8 ; :: thesis: verum

end;

hence n -BinarySequence 0 = ZERO n by A1, A3, FINSEQ_2:10; :: thesis: verum