defpred S1[ Nat] means for i2 being Integer st $1 = i2 - F1() holds
P1[i2];
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
reconsider i8 =
k as
Integer ;
assume A4:
S1[
k]
;
S1[k + 1]
let i2 be
Integer;
( k + 1 = i2 - F1() implies P1[i2] )
assume A5:
k + 1
= i2 - F1()
;
P1[i2]
then
i2 - 1
= i8 + F1()
;
then A6:
F1()
<= i2 - 1
by Th6;
k = (i2 - 1) - F1()
by A5;
then
P1[
(i2 - 1) + 1]
by A2, A4, A6;
hence
P1[
i2]
;
verum
end;
let i0 be Integer; ( F1() <= i0 implies P1[i0] )
assume
F1() <= i0
; P1[i0]
then reconsider l = i0 - F1() as Element of NAT by Th5;
A7:
l = i0 - F1()
;
A8:
S1[ 0 ]
by A1;
for k being Nat holds S1[k]
from NAT_1:sch 2(A8, A3);
hence
P1[i0]
by A7; verum