let n, i be Element of 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₁[ Element of 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 by FUNCT_1:18 ;
then A1: S₁[ 0 ] ;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1] by Th38;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
hence dom f = dom (((repeat ((Relax n) * (findmin n))) . i) . f) ; :: thesis: verum