let n, i, k be Element of NAT ; :: thesis: for g, f, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . i) . f & h = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f & k = Argmin (OuterVx g,n),g,n & OuterVx g,n <> {} holds
( UsedVx h,n = (UsedVx g,n) \/ {k} & not k in UsedVx g,n )
let g, f, h be Element of REAL * ; :: thesis: ( g = ((repeat ((Relax n) * (findmin n))) . i) . f & h = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f & k = Argmin (OuterVx g,n),g,n & OuterVx g,n <> {} implies ( UsedVx h,n = (UsedVx g,n) \/ {k} & not k in UsedVx g,n ) )
set R = Relax n;
set M = findmin n;
set ff = ((repeat ((Relax n) * (findmin n))) . i) . f;
set Fi1 = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f;
set mi = ((n * n) + (3 * n)) + 1;
assume A1: ( g = ((repeat ((Relax n) * (findmin n))) . i) . f & h = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f & k = Argmin (OuterVx g,n),g,n & OuterVx g,n <> {} ) ; :: thesis: ( UsedVx h,n = (UsedVx g,n) \/ {k} & not k in UsedVx g,n )
then A2: dom h = dom (((repeat ((Relax n) * (findmin n))) . i) . f) by Th38;
then A3: dom h = dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) by Th34;
A4: (findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f) = (((repeat ((Relax n) * (findmin n))) . i) . f),(((n * n) + (3 * n)) + 1) := k,(- 1) by A1, Def11;
A5: dom g = dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) by A1, Th34;

A6: now

let x be set ; :: thesis: ( x in UsedVx h,n implies b₁ in (UsedVx g,n) \/ {k} )
assume x in UsedVx h,n ; :: thesis: b₁ in (UsedVx g,n) \/ {k}
then consider m being Element of NAT such that
A7: ( x = m & m in dom h & 1 <= m & m <= n & h . m = - 1 ) ;

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

suppose m = k ; :: thesis: b₁ in (UsedVx g,n) \/ {k}

then x in {k} by A7, TARSKI:def 1;
hence x in (UsedVx g,n) \/ {k} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A8: m <> k ; :: thesis: b₁ in (UsedVx g,n) \/ {k}

A9: n < ((n * n) + (3 * n)) + 1 by Lm7;
A10: m in dom (((repeat ((Relax n) * (findmin n))) . i) . f) by A1, A7, Th38;
- 1 = ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . m by A1, A7, Th23
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . m by A3, A7, Th37
.= (((repeat ((Relax n) * (findmin n))) . i) . f) . m by A4, A7, A8, A9, A10, Th19 ;
then m in { j where j is Element of NAT : ( j in dom (((repeat ((Relax n) * (findmin n))) . i) . f) & 1 <= j & j <= n & (((repeat ((Relax n) * (findmin n))) . i) . f) . j = - 1 ) } by A2, A7;
hence x in (UsedVx g,n) \/ {k} by A1, A7, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

now

let x be set ; :: thesis: ( x in (UsedVx g,n) \/ {k} implies b₁ in UsedVx h,n )
assume A11: x in (UsedVx g,n) \/ {k} ; :: thesis: b₁ in UsedVx h,n

per cases ( x in UsedVx g,n or x in {k} ) by A11, XBOOLE_0:def 3;

suppose x in UsedVx g,n ; :: thesis: b₁ in UsedVx h,n

then consider m being Element of NAT such that
A12: ( x = m & m in dom g & 1 <= m & m <= n & g . m = - 1 ) ;
A13: n < ((n * n) + (3 * n)) + 1 by Lm7;
h . m = ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . m by A1, Th23
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . m by A5, A12, Th37
.= - 1 by A1, A12, A13, Th33 ;
hence x in UsedVx h,n by A1, A2, A12; :: thesis: verum

end;

suppose x in {k} ; :: thesis: b₁ in UsedVx h,n

then A14: x = k by TARSKI:def 1;
A15: ( k in dom g & 1 <= k & k <= n ) by A1, Th30;
h . k = ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . k by A1, Th23
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . k by A5, A15, Th37
.= - 1 by A1, A4, A15, Th20 ;
hence x in UsedVx h,n by A1, A2, A14, A15; :: thesis: verum

end;

end;

end;

hence UsedVx h,n = (UsedVx g,n) \/ {k} by A6, TARSKI:2; :: thesis: not k in UsedVx g,n
assume k in UsedVx g,n ; :: thesis: contradiction
then consider j being Element of NAT such that
A16: ( j = k & j in dom g & 1 <= j & j <= n & g . j = - 1 ) ;
thus contradiction by A1, A16, Th30; :: thesis: verum