let i, n be 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₁[ 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 S₁[k] holds
S₁[k + 1]

proof

let k be 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 Th44;
hence S₁[k + 1] by A2, Th43; :: thesis: verum

end;

((repeat ((Relax n) * (findmin n))) . 0) . f = f by Th21;
then A3: S₁[ 0 ] by Th42;
for k being Nat holds S₁[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) ; :: thesis: verum