let i, n be Nat; :: thesis: for f being Element of REAL * holds dom (((repeat ((Relax n) * (findmin n))) . i) . f) = dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f)
let f be Element of REAL * ; :: thesis: dom (((repeat ((Relax n) * (findmin n))) . i) . f) = dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f)
set R = Relax n;
set M = findmin n;
set ff = ((repeat ((Relax n) * (findmin n))) . i) . f;
thus dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) = dom ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) by Th22
.= dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) by Th35
.= dom (((repeat ((Relax n) * (findmin n))) . i) . f) by Th33 ; :: thesis: verum