let i, n be Nat; :: thesis: for f being Element of REAL * holds ((repeat ((Relax n) * (findmin n))) . i) . f,((repeat ((Relax n) * (findmin n))) . (i + 1)) . f equal_at (3 * n) + 1,(n * n) + (3 * n)
let f be Element of REAL * ; :: thesis: ((repeat ((Relax n) * (findmin n))) . i) . f,((repeat ((Relax n) * (findmin n))) . (i + 1)) . f equal_at (3 * n) + 1,(n * n) + (3 * n)
set R = Relax n;
set M = findmin n;
set ff = ((repeat ((Relax n) * (findmin n))) . i) . f;
set Fi1 = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f;

A1: now :: thesis: for k being Nat st k in dom (((repeat ((Relax n) * (findmin n))) . i) . f) & (3 * n) + 1 <= k & k <= (n * n) + (3 * n) holds
(((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) . k = (((repeat ((Relax n) * (findmin n))) . i) . f) . k

let k be Nat; :: thesis: ( k in dom (((repeat ((Relax n) * (findmin n))) . i) . f) & (3 * n) + 1 <= k & k <= (n * n) + (3 * n) implies (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) . k = (((repeat ((Relax n) * (findmin n))) . i) . f) . k )
assume that
A2: k in dom (((repeat ((Relax n) * (findmin n))) . i) . f) and
A3: (3 * n) + 1 <= k and
A4: k <= (n * n) + (3 * n) ; :: thesis: (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) . k = (((repeat ((Relax n) * (findmin n))) . i) . f) . k
A5: k > 3 * n by A3, NAT_1:13;
A6: k in dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) by A2, Th33;
A7: k < ((n * n) + (3 * n)) + 1 by A4, NAT_1:13;
3 * n >= n by Lm6;
then A8: k > n by A5, XXREAL_0:2;
thus (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) . k = ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . k by Th22
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . k by A5, A6, Th36
.= (((repeat ((Relax n) * (findmin n))) . i) . f) . k by A7, A8, Th31 ; :: thesis: verum

end;

dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) = dom (((repeat ((Relax n) * (findmin n))) . i) . f) by Th37;
hence ((repeat ((Relax n) * (findmin n))) . i) . f,((repeat ((Relax n) * (findmin n))) . (i + 1)) . f equal_at (3 * n) + 1,(n * n) + (3 * n) by A1; :: thesis: verum