let m be non empty Nat; :: thesis: Bin1 (m + 1) = (Bin1 m) ^ <*FALSE*>
A1: ( len (Bin1 (m + 1)) = m + 1 & len ((Bin1 m) ^ <*FALSE*>) = m + 1 ) by FINSEQ_1:def 18;
for i being Nat st i in Seg (m + 1) holds
(Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i

proof

let i be Nat; :: thesis: ( i in Seg (m + 1) implies (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i )
assume A3: i in Seg (m + 1) ; :: thesis: (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i

per cases ( i in Seg m or i = m + 1 ) by A3, FINSEQ_2:8;

suppose A4: i in Seg m ; :: thesis: (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i

thus (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i :: thesis: verum

proof

per cases ( i = 1 or i <> 1 ) ;

suppose A5: i = 1 ; :: thesis: (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i

((Bin1 m) ^ <*FALSE*>) /. i = (Bin1 m) /. i by A4, BINARITH:2
.= TRUE by A4, A5, Th7 ;
hence (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i by A3, A5, Th7; :: thesis: verum

end;

suppose A7: i <> 1 ; :: thesis: (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i

((Bin1 m) ^ <*FALSE*>) /. i = (Bin1 m) /. i by A4, BINARITH:2
.= FALSE by A4, A7, Th8 ;
hence (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i by A3, A7, Th8; :: thesis: verum

end;

end;

end;

end;

suppose A9: i = m + 1 ; :: thesis: (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i

1 <> m + 1 by NAT_1:14;
then (Bin1 (m + 1)) /. i = FALSE by A3, A9, Th8;
hence (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i by A9, BINARITH:3; :: thesis: verum

end;

end;

end;

hence Bin1 (m + 1) = (Bin1 m) ^ <*FALSE*> by A1, Lm1; :: thesis: verum