let m be non zero Nat; :: thesis: Bin1 (m + 1) = (Bin1 m) ^ <*FALSE*>
A1: ( len (Bin1 (m + 1)) = m + 1 & len ((Bin1 m) ^ <*FALSE*>) = m + 1 ) by CARD_1:def 7;
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 A2: 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 A2, FINSEQ_2:7;

suppose A3: 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 A4: i = 1 ; :: thesis: (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i

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

end;

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

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

end;

end;

end;

end;

suppose A6: 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 A2, A6, Th6;
hence (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE*>) /. i by A6, BINARITH:2; :: thesis: verum

end;

end;

end;

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