let n be Element of NAT ; :: thesis: n -BinarySequence 0 = ZERO n
A1: ( len (n -BinarySequence 0 ) = n & len (ZERO n) = n ) by FINSEQ_1:def 18;
then A2: ( dom (n -BinarySequence 0 ) = Seg n & dom (ZERO n) = Seg n ) by FINSEQ_1:def 3;
X: 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 )
assume A3: j in dom (n -BinarySequence 0 ) ; :: thesis: (n -BinarySequence 0 ) . j = (ZERO n) . j
A4: (0 div (2 to_power (j -' 1))) mod 2 = 0 mod 2 by NAT_2:4
.= 0 by NAT_D:26 ;
j in dom (ZERO n) by A3, X, FUNCOP_1:19;
then A5: (ZERO n) /. j = (n |-> FALSE ) . j by PARTFUN1:def 8
.= FALSE by A3, X, FUNCOP_1:13 ;
thus (n -BinarySequence 0 ) . j = (n -BinarySequence 0 ) /. j by A3, PARTFUN1:def 8
.= IFEQ ((0 div (2 to_power (j -' 1))) mod 2),0 ,FALSE ,TRUE by A3, X, BINARI_3:def 1
.= (ZERO n) /. j by A4, A5, FUNCOP_1:def 8
.= (ZERO n) . j by A2, A3, PARTFUN1:def 8 ; :: thesis: verum

end;

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