defpred S1[ Nat] means for z being Tuple of $1, BOOLEAN st z /. $1 = TRUE holds
Absval z >= 2 to_power ($1 -' 1);
A1:
for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non
zero Nat;
( S1[n] implies S1[n + 1] )
assume
S1[
n]
;
S1[n + 1]
let z be
Tuple of
n + 1,
BOOLEAN ;
( z /. (n + 1) = TRUE implies Absval z >= 2 to_power ((n + 1) -' 1) )
assume A2:
z /. (n + 1) = TRUE
;
Absval z >= 2 to_power ((n + 1) -' 1)
consider x being
Element of
n -tuples_on BOOLEAN,
a being
Element of
BOOLEAN such that A3:
z = x ^ <*a*>
by FINSEQ_2:117;
A4:
n + 1
>= 1
by NAT_1:11;
then
(n + 1) - 1
>= 1
- 1
by XREAL_1:9;
then A5:
(n + 1) -' 1
= n
by XREAL_0:def 2;
len z = n + 1
by CARD_1:def 7;
then A6:
z /. (n + 1) =
(x ^ <*a*>) . (n + 1)
by A3, A4, FINSEQ_4:15
.=
a
by FINSEQ_2:116
;
Absval z =
(Absval x) + (IFEQ (a,FALSE,0,(2 to_power n)))
by A3, BINARITH:20
.=
(Absval x) + (2 to_power n)
by A2, A6, FUNCOP_1:def 8
;
hence
Absval z >= 2
to_power ((n + 1) -' 1)
by A5, NAT_1:11;
verum
end;
A7:
S1[1]
thus
for n being non zero Nat holds S1[n]
from NAT_1:sch 10(A7, A1); verum