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: 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;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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 < 2 to_power n by NAT_1:13;
0* n in BOOLEAN * by Th5;
then A6: 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
len (0* n) = n by FINSEQ_1:def 18;
then reconsider 0n = 0* n as Tuple of n,BOOLEAN by A6, FINSEQ_2:110;
(k + 1) - 1 < (2 to_power n) - 1 by A4, XREAL_1:11;
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 A7: 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 A7, BINARITH:48
.= k + 1 by A3, A4, Th12, NAT_1:13 ; :: thesis: verum

end;

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