let i, m, n be Nat; :: thesis: 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)
let f, g, h be Element of REAL * ; :: thesis: ( 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) implies m in UsedVx (h,n) )
set RF = (Relax n) * (findmin n);
set RT = repeat ((Relax n) * (findmin n));
set cn = LifeSpan (((Relax n) * (findmin n)),f,n);
assume that
A1: g = ((repeat ((Relax n) * (findmin n))) . 1) . f and
A2: ( h = ((repeat ((Relax n) * (findmin n))) . i) . f & 1 <= i & i <= LifeSpan (((Relax n) * (findmin n)),f,n) ) and
A3: m in UsedVx (g,n) ; :: thesis: m in UsedVx (h,n)
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= LifeSpan (((Relax n) * (findmin n)),f,n) implies m in UsedVx ((((repeat ((Relax n) * (findmin n))) . $1) . f),n) );
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]

hereby :: thesis: verum

assume that
1 <= k + 1 and
A6: k + 1 <= LifeSpan (((Relax n) * (findmin n)),f,n) ; :: thesis: m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n)

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n)

hence m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) by A1, A3; :: thesis: verum

end;

suppose A7: k <> 0 ; :: thesis: m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n)

k < LifeSpan (((Relax n) * (findmin n)),f,n) by A6, NAT_1:13;
then OuterVx ((((repeat ((Relax n) * (findmin n))) . k) . f),n) <> {} by Def4;
then UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) = (UsedVx ((((repeat ((Relax n) * (findmin n))) . k) . f),n)) \/ {(Argmin ((OuterVx ((((repeat ((Relax n) * (findmin n))) . k) . f),n)),(((repeat ((Relax n) * (findmin n))) . k) . f),n))} by Th39;
then A8: UsedVx ((((repeat ((Relax n) * (findmin n))) . k) . f),n) c= UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) by XBOOLE_1:7;
k >= 1 + 0 by A7, INT_1:7;
hence m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) by A5, A6, A8, NAT_1:13; :: thesis: verum

end;

end;

end;

end;

A9: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A4);
hence m in UsedVx (h,n) by A2; :: thesis: verum