let i0 be Integer; :: thesis: P₁[i0]
A3: P₁[F₁()] by A1;

A4: now :: thesis: ( i0 <= F₁() implies P₁[i0] )

A5: for i2 being Integer st i2 <= F₁() & P₁[i2] holds
P₁[i2 - 1] by A2;
A6: for i2 being Integer st i2 <= F₁() holds
P₁[i2] from INT_1:sch 3(A3, A5);
assume i0 <= F₁() ; :: thesis: P₁[i0]
hence P₁[i0] by A6; :: thesis: verum

end;

now :: thesis: ( F₁() <= i0 implies P₁[i0] )

A7: for i2 being Integer st F₁() <= i2 & P₁[i2] holds
P₁[i2 + 1] by A2;
A8: for i2 being Integer st F₁() <= i2 holds
P₁[i2] from INT_1:sch 2(A3, A7);
assume F₁() <= i0 ; :: thesis: P₁[i0]
hence P₁[i0] by A8; :: thesis: verum

end;

hence P₁[i0] by A4; :: thesis: verum