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 ;

now :: thesis: for i being Nat st i in Seg n holds
(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)
.= 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;

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