defpred S1[ Element of NAT ] means for j being Element of NAT st F1() <= j & j <= $1 holds
P1[j];
A3:
for j being Element of NAT st F1() <= j & j < F2() & S1[j] holds
S1[j + 1]
proof
let j be
Element of
NAT ;
( F1() <= j & j < F2() & S1[j] implies S1[j + 1] )
assume that A4:
F1()
<= j
and A5:
j < F2()
;
( not S1[j] or S1[j + 1] )
assume A6:
S1[
j]
;
S1[j + 1]
thus
S1[
j + 1]
verumproof
let i be
Element of
NAT ;
( F1() <= i & i <= j + 1 implies P1[i] )
assume that A7:
F1()
<= i
and A8:
i <= j + 1
;
P1[i]
end;
end;
A9:
S1[F1()]
by A1, XXREAL_0:1;
for i being Element of NAT st F1() <= i & i <= F2() holds
S1[i]
from INT_1:sch 7(A9, A3);
hence
for i being Element of NAT st F1() <= i & i <= F2() holds
P1[i]
; verum