for i, m, n being Nat
for f, g, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . 1) . f & h = ((repeat ((Relax n) * (findmin n))) . i) . f & 1 <= i & i <= LifeSpan (((Relax n) * (findmin n)),f,n) & m in UsedVx (g,n) holds
m in UsedVx (h,n)