let n be Nat; :: thesis: n -BinarySequence 0 = ZERO n
A1: len (n -BinarySequence 0) = n by CARD_1:def 7;
then A2: dom (n -BinarySequence 0) = Seg n by FINSEQ_1:def 3;
A3: len (ZERO n) = n by CARD_1:def 7;
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 :: thesis: for j being Nat st j in dom (n -BinarySequence 0) holds
(n -BinarySequence 0) . j = (ZERO n) . j

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
.= 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:13;
then A8: (ZERO n) /. j = (n |-> FALSE) . j by PARTFUN1:def 6
.= FALSE ;
thus (n -BinarySequence 0) . j = (n -BinarySequence 0) /. j by A7, PARTFUN1:def 6
.= 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 6 ; :: thesis: verum

end;

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