let i0 be Integer; :: thesis: P1[i0]
A3: P1[F1()] by A1;
A4: now :: thesis: ( i0 <= F1() implies P1[i0] )
A5: for i2 being Integer st i2 <= F1() & P1[i2] holds
P1[i2 - 1] by A2;
A6: for i2 being Integer st i2 <= F1() holds
P1[i2] from INT_1:sch 3(A3, A5);
assume i0 <= F1() ; :: thesis: P1[i0]
hence P1[i0] by A6; :: thesis: verum
end;
now :: thesis: ( F1() <= i0 implies P1[i0] )
A7: for i2 being Integer st F1() <= i2 & P1[i2] holds
P1[i2 + 1] by A2;
A8: for i2 being Integer st F1() <= i2 holds
P1[i2] from INT_1:sch 2(A3, A7);
assume F1() <= i0 ; :: thesis: P1[i0]
hence P1[i0] by A8; :: thesis: verum
end;
hence P1[i0] by A4; :: thesis: verum