let n be non zero 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 Th4;
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 A2: ( k < 2 to_power n implies Absval (n -BinarySequence k) = k ) ; :: thesis: S₁[k + 1]
assume A3: k + 1 < 2 to_power n ; :: thesis: Absval (n -BinarySequence (k + 1)) = k + 1
then A4: (k + 1) - 1 < (2 to_power n) - 1 by XREAL_1:9;
k < 2 to_power n by A3, NAT_1:13;
then n -BinarySequence k <> 'not' 0n by A4, Lm4;
then add_ovfl ((n -BinarySequence k),(Bin1 n)) <> TRUE by Th23;
then add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE by XBOOLEAN:def 3;
then A5: n -BinarySequence k, Bin1 n are_summable by BINARITH:def 7;
thus Absval (n -BinarySequence (k + 1)) = Absval ((n -BinarySequence k) + (Bin1 n)) by A3, Th33
.= (Absval (n -BinarySequence k)) + (Absval (Bin1 n)) by A5, BINARITH:22
.= k + 1 by A2, A3, Th11, NAT_1:13 ; :: thesis: verum

end;

A6: S₁[ 0 ]

proof

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

end;

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