let m be non empty Nat; :: thesis: Bin1 (m + 1) = (Bin1 m) ^ <*FALSE *>
A1: len (Bin1 (m + 1)) = m + 1 by FINSEQ_1:def 18;
A2: 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 A6: 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, A6, Th8 ;
hence (Bin1 (m + 1)) /. i = ((Bin1 m) ^ <*FALSE *>) /. i by A3, A6, Th8; :: thesis: verum

end;

end;

end;

end;

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

end;

end;

end;

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