defpred S₁[ Element of NAT ] means for j being Element of NAT st F₁() <= j & j <= $1 holds
P₁[j];
A3: for j being Element of NAT st F₁() <= j & j < F₂() & S₁[j] holds
S₁[j + 1]

proof

let j be Element of NAT ; :: thesis: ( F₁() <= j & j < F₂() & S₁[j] implies S₁[j + 1] )
assume that
A4: F₁() <= j and
A5: j < F₂() ; :: thesis: ( not S₁[j] or S₁[j + 1] )
assume A6: S₁[j] ; :: thesis: S₁[j + 1]
thus S₁[j + 1] :: thesis: verum

proof

let i be Element of NAT ; :: thesis: ( F₁() <= i & i <= j + 1 implies P₁[i] )
assume that
A7: F₁() <= i and
A8: i <= j + 1 ; :: thesis: P₁[i]

per cases ( i = j + 1 or i <> j + 1 ) ;

suppose i = j + 1 ; :: thesis: P₁[i]

hence P₁[i] by A2, A4, A5, A6; :: thesis: verum

end;

suppose i <> j + 1 ; :: thesis: P₁[i]

then i < j + 1 by A8, XXREAL_0:1;
then i <= j by NAT_1:13;
hence P₁[i] by A6, A7; :: thesis: verum

end;

end;

end;

end;

A9: S₁[F₁()] by A1, XXREAL_0:1;
for i being Element of NAT st F₁() <= i & i <= F₂() holds
S₁[i] from INT_1:sch 7(A9, A3);
hence for i being Element of NAT st F₁() <= i & i <= F₂() holds
P₁[i] ; :: thesis: verum