let n be Nat; :: thesis: n -BinarySequence 0 = 0* n

0* n in BOOLEAN * by Th4;

then 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;

then reconsider F = 0* n as Tuple of n, BOOLEAN ;

0* n in BOOLEAN * by Th4;

then 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;

then reconsider F = 0* n as Tuple of n, BOOLEAN ;

now :: thesis: for i being Nat st i in Seg n holds

(n -BinarySequence 0) . i = F . i

hence
n -BinarySequence 0 = 0* n
by FINSEQ_2:119; :: thesis: verum(n -BinarySequence 0) . i = F . i

let i be Nat; :: thesis: ( i in Seg n implies (n -BinarySequence 0) . i = F . i )

assume A1: i in Seg n ; :: thesis: (n -BinarySequence 0) . i = F . i

len (n -BinarySequence 0) = n by CARD_1:def 7;

then i in dom (n -BinarySequence 0) by A1, FINSEQ_1:def 3;

hence (n -BinarySequence 0) . i = (n -BinarySequence 0) /. i by PARTFUN1:def 6

.= IFEQ (((0 div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A1, Def1

.= IFEQ ((0 mod 2),0,FALSE,TRUE) by NAT_2:2

.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26

.= 0 by FUNCOP_1:def 8

.= F . i by A1, FUNCOP_1:7 ;

:: thesis: verum

end;assume A1: i in Seg n ; :: thesis: (n -BinarySequence 0) . i = F . i

len (n -BinarySequence 0) = n by CARD_1:def 7;

then i in dom (n -BinarySequence 0) by A1, FINSEQ_1:def 3;

hence (n -BinarySequence 0) . i = (n -BinarySequence 0) /. i by PARTFUN1:def 6

.= IFEQ (((0 div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A1, Def1

.= IFEQ ((0 mod 2),0,FALSE,TRUE) by NAT_2:2

.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26

.= 0 by FUNCOP_1:def 8

.= F . i by A1, FUNCOP_1:7 ;

:: thesis: verum