let n be non empty Nat; :: thesis: for k being Nat st k < 2 to_power n holds
Absval (n -BinarySequence k) = k
defpred S₁[ Nat] means ( $1 < 2 to_power n implies Absval (n -BinarySequence $1) = $1 );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

0* n in BOOLEAN * by Th5;
then 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
then reconsider 0n = 0* n as Tuple of n, BOOLEAN ;
let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: ( k < 2 to_power n implies Absval (n -BinarySequence k) = k ) ; :: thesis: S₁[k + 1]
assume A4: k + 1 < 2 to_power n ; :: thesis: Absval (n -BinarySequence (k + 1)) = k + 1
then A5: (k + 1) - 1 < (2 to_power n) - 1 by XREAL_1:11;
k < 2 to_power n by A4, NAT_1:13;
then n -BinarySequence k <> 'not' 0n by A5, Lm4;
then add_ovfl (n -BinarySequence k),(Bin1 n) <> TRUE by Th24;
then add_ovfl (n -BinarySequence k),(Bin1 n) = FALSE by XBOOLEAN:def 3;
then A6: n -BinarySequence k, Bin1 n are_summable by BINARITH:def 10;
thus Absval (n -BinarySequence (k + 1)) = Absval ((n -BinarySequence k) + (Bin1 n)) by A4, Th34
.= (Absval (n -BinarySequence k)) + (Absval (Bin1 n)) by A6, BINARITH:48
.= k + 1 by A3, A4, Th12, NAT_1:13 ; :: thesis: verum

end;

A7: S₁[ 0 ]

proof

assume 0 < 2 to_power n ; :: thesis: Absval (n -BinarySequence 0 ) = 0
n -BinarySequence 0 = 0* n by Th26;
hence Absval (n -BinarySequence 0 ) = 0 by Th7; :: thesis: verum

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A1); :: thesis: verum