let n, i be Element of NAT ; :: thesis: 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 * ; :: thesis: 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 S₁[ Element of NAT ] means f,((repeat ((Relax n) * (findmin n))) . $1) . f equal_at (3 * n) + 1,(n * n) + (3 * n);
A1: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
((repeat ((Relax n) * (findmin n))) . k) . f,((repeat ((Relax n) * (findmin n))) . (k + 1)) . f equal_at (3 * n) + 1,(n * n) + (3 * n) by Th45;
hence S₁[k + 1] by A2, Th44; :: thesis: verum

end;

((repeat ((Relax n) * (findmin n))) . 0) . f = f by Th22;
then A3: S₁[ 0 ] by Th43;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A1);
hence f,((repeat ((Relax n) * (findmin n))) . i) . f equal_at (3 * n) + 1,(n * n) + (3 * n) ; :: thesis: verum