let i, n be Nat; :: thesis: for f being Element of REAL * holds dom f = dom (((repeat ((Relax n) * (findmin n))) . i) . f)
let f be Element of REAL * ; :: thesis: dom f = dom (((repeat ((Relax n) * (findmin n))) . i) . f)
set R = Relax n;
set M = findmin n;
defpred S₁[ Nat] means dom f = dom (((repeat ((Relax n) * (findmin n))) . $1) . f);
dom (((repeat ((Relax n) * (findmin n))) . 0) . f) = dom ((id (REAL *)) . f) by Def2
.= dom f ;
then A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1] by Th37;
for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence dom f = dom (((repeat ((Relax n) * (findmin n))) . i) . f) ; :: thesis: verum