let i, n be Nat; for f being Element of REAL * holds f,((repeat ((Relax n) * (findmin n))) . i) . f equal_at (3 * n) + 1,(n * n) + (3 * n)
let f be Element of REAL * ; f,((repeat ((Relax n) * (findmin n))) . i) . f equal_at (3 * n) + 1,(n * n) + (3 * n)
set R = Relax n;
set M = findmin n;
set m = (3 * n) + 1;
set mm = (n * n) + (3 * n);
defpred S1[ Nat] means f,((repeat ((Relax n) * (findmin n))) . $1) . f equal_at (3 * n) + 1,(n * n) + (3 * n);
A1:
for k being Nat st S1[k] holds
S1[k + 1]
((repeat ((Relax n) * (findmin n))) . 0) . f = f
by Th21;
then A3:
S1[ 0 ]
by Th42;
for k being Nat holds S1[k]
from NAT_1:sch 2(A3, A1);
hence
f,((repeat ((Relax n) * (findmin n))) . i) . f equal_at (3 * n) + 1,(n * n) + (3 * n)
; verum