let i, k, n be Nat; :: thesis: for f, g, 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 f, g, 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 that
A1: g = ((repeat ((Relax n) * (findmin n))) . i) . f and
A2: h = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f and
A3: k = Argmin ((OuterVx (g,n)),g,n) and
A4: OuterVx (g,n) <> {} ; :: thesis: ( UsedVx (h,n) = (UsedVx (g,n)) \/ {k} & not k in UsedVx (g,n) )
A5: (findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f) = ((((repeat ((Relax n) * (findmin n))) . i) . f),(((n * n) + (3 * n)) + 1)) := (k,(- jj)) by A1, A3, Def11;
A6: dom h = dom (((repeat ((Relax n) * (findmin n))) . i) . f) by A2, Th37;
A7: dom g = dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) by A1, Th33;

A8: now :: thesis: for x being object st x in (UsedVx (g,n)) \/ {k} holds
x in UsedVx (h,n)

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

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

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

A11: n < ((n * n) + (3 * n)) + 1 by Lm7;
consider m being Nat such that
A12: x = m and
A13: m in dom g and
A14: 1 <= m and
A15: m <= n and
A16: g . m = - 1 by A10;
h . m = ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . m by A2, Th22
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . m by A7, A13, A15, Th36
.= - 1 by A1, A13, A15, A16, A11, Th32 ;
hence x in UsedVx (h,n) by A1, A6, A12, A13, A14, A15; :: thesis: verum

end;

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

then A17: x = k by TARSKI:def 1;
A18: k in dom g by A3, A4, Th29;
A19: 1 <= k by A3, A4, Th29;
A20: k <= n by A3, A4, Th29;
h . k = ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . k by A2, Th22
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . k by A7, A18, A20, Th36
.= - jj by A1, A5, A18, Th19 ;
hence x in UsedVx (h,n) by A1, A6, A17, A18, A19, A20; :: thesis: verum

end;

end;

end;

A21: dom h = dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) by A6, Th33;

now :: thesis: for x being object st x in UsedVx (h,n) holds
x in (UsedVx (g,n)) \/ {k}

let x be object ; :: 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 Nat such that
A22: x = m and
A23: m in dom h and
A24: 1 <= m and
A25: m <= n and
A26: 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 A22, TARSKI:def 1;
hence x in (UsedVx (g,n)) \/ {k} by XBOOLE_0:def 3; :: thesis: verum

end;

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

A28: n < ((n * n) + (3 * n)) + 1 by Lm7;
- 1 = ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . m by A2, A26, Th22
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . m by A21, A23, A25, Th36
.= (((repeat ((Relax n) * (findmin n))) . i) . f) . m by A5, A25, A27, A28, Th18 ;
then m in { j where j is 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 A6, A23, A24, A25;
hence x in (UsedVx (g,n)) \/ {k} by A1, A22, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence UsedVx (h,n) = (UsedVx (g,n)) \/ {k} by A8, TARSKI:2; :: thesis: not k in UsedVx (g,n)
assume k in UsedVx (g,n) ; :: thesis: contradiction
then ex j being Nat st
( j = k & j in dom g & 1 <= j & j <= n & g . j = - 1 ) ;
hence contradiction by A3, A4, Th29; :: thesis: verum