let n be Nat; :: thesis: n -BinarySequence 0 = 0* n
0* n in BOOLEAN * by Th5;
then 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
then reconsider F = 0* n as Tuple of n, BOOLEAN ;

now

let i be Nat; :: thesis: ( i in Seg n implies (n -BinarySequence 0 ) . i = F . i )
assume A2: i in Seg n ; :: thesis: (n -BinarySequence 0 ) . i = F . i
len (n -BinarySequence 0 ) = n by FINSEQ_1:def 18;
then i in dom (n -BinarySequence 0 ) by A2, FINSEQ_1:def 3;
hence (n -BinarySequence 0 ) . i = (n -BinarySequence 0 ) /. i by PARTFUN1:def 8
.= IFEQ ((0 div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE by A2, Def1
.= IFEQ (0 mod 2),0 ,FALSE ,TRUE by NAT_2:4
.= IFEQ 0 ,0 ,FALSE ,TRUE by NAT_D:26
.= 0 by FUNCOP_1:def 8
.= F . i by A2, FUNCOP_1:13 ;
:: thesis: verum

end;

hence n -BinarySequence 0 = 0* n by FINSEQ_2:139; :: thesis: verum