let n, i, m be Element of NAT ; :: thesis: for g, f, 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 g, f, 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₁[ Element of 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 Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of 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 Th40;
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:20;
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 Element of NAT holds S₁[k] from NAT_1:sch 1(A9, A4);
hence m in UsedVx h,n by A2; :: thesis: verum