deffunc H₁( Nat) -> Tuple of $1 + 1, BOOLEAN = ($1 + 1) -BinarySequence (2 to_power $1);
let i be Nat; :: thesis: (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*>
set Bi = H₁(i);

per cases ( i = 0 or i > 0 ) ;

suppose A1: i = 0 ; :: thesis: (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*>

then A2: 0* i = 0 ;
reconsider i1 = i + 1 as non zero Nat ;
A3: 0* i1 = <*FALSE*> by A1, FINSEQ_2:59;
then reconsider x = 0* i1 as Tuple of i1, BOOLEAN ;
2 to_power i1 = 2 by A1, POWER:25;
then 1 = (2 to_power i1) - 1 ;
then i1 -BinarySequence 1 = 'not' x by Lm4;
hence H₁(i) = <*TRUE*> by A1, A3, Th14, POWER:24
.= (0* i) ^ <*1*> by A2, FINSEQ_1:34 ;
:: thesis: verum

end;

suppose i > 0 ; :: thesis: (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*>

then reconsider i9 = i as non zero Nat ;
H₁(i) = (0* i9) ^ <*1*> by Lm1;
hence (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*> ; :: thesis: verum

end;

end;