let n be Nat; 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 for j being Nat st j in dom (n -BinarySequence 0) holds
(n -BinarySequence 0) . j = (ZERO n) . jlet j be
Nat;
( 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:2
.=
0
by NAT_D:26
;
assume A7:
j in dom (n -BinarySequence 0)
;
(n -BinarySequence 0) . j = (ZERO n) . jthen
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
;
verum end;
hence
n -BinarySequence 0 = ZERO n
by A1, A3, FINSEQ_2:9; verum