let n be Nat; :: thesis: for f being Element of REAL * st 1 <= n & 1 in dom f & f . (n + 1) <> - 1 & ( for i being Nat st 1 <= i & i <= n holds
f . i = 1 ) & ( for i being Nat st 2 <= i & i <= n holds
f . (n + i) = - 1 ) holds
( 1 = Argmin ((OuterVx (f,n)),f,n) & UsedVx (f,n) = {} & {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) )
let f be Element of REAL * ; :: thesis: ( 1 <= n & 1 in dom f & f . (n + 1) <> - 1 & ( for i being Nat st 1 <= i & i <= n holds
f . i = 1 ) & ( for i being Nat st 2 <= i & i <= n holds
f . (n + i) = - 1 ) implies ( 1 = Argmin ((OuterVx (f,n)),f,n) & UsedVx (f,n) = {} & {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) ) )
set R = Relax n;
set M = findmin n;
set f0 = ((repeat ((Relax n) * (findmin n))) . 0) . f;
set RT = repeat ((Relax n) * (findmin n));
assume that
A1: 1 <= n and
A2: ( 1 in dom f & f . (n + 1) <> - 1 ) and
A3: for i being Nat st 1 <= i & i <= n holds
f . i = 1 and
A4: for i being Nat st 2 <= i & i <= n holds
f . (n + i) = - 1 ; :: thesis: ( 1 = Argmin ((OuterVx (f,n)),f,n) & UsedVx (f,n) = {} & {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) )
set k = Argmin ((OuterVx (f,n)),f,n);
f . 1 = 1 by A1, A3;
then A5: 1 in { j where j is Nat : ( j in dom f & 1 <= j & j <= n & f . j <> - 1 & f . (n + j) <> - 1 ) } by A1, A2;
thus A6: Argmin ((OuterVx (f,n)),f,n) = 1 :: thesis: ( UsedVx (f,n) = {} & {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) )

proof

assume A7: Argmin ((OuterVx (f,n)),f,n) <> 1 ; :: thesis: contradiction
1 <= Argmin ((OuterVx (f,n)),f,n) by A5, Th29;
then 1 < Argmin ((OuterVx (f,n)),f,n) by A7, XXREAL_0:1;
then A8: 1 + 1 <= Argmin ((OuterVx (f,n)),f,n) by INT_1:7;
( Argmin ((OuterVx (f,n)),f,n) <= n & f . (n + (Argmin ((OuterVx (f,n)),f,n))) <> - 1 ) by A5, Th29;
hence contradiction by A4, A8; :: thesis: verum

end;

thus A9: UsedVx (f,n) = {} :: thesis: {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n)

proof

assume UsedVx (f,n) <> {} ; :: thesis: contradiction
then consider x being object such that
A10: x in UsedVx (f,n) by XBOOLE_0:def 1;
ex j being Nat st
( x = j & j in dom f & 1 <= j & j <= n & f . j = - 1 ) by A10;
hence contradiction by A3; :: thesis: verum

end;

OuterVx (f,n) <> {} by A5;
then A11: OuterVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n) <> {} by Th21;
A12: Argmin ((OuterVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n)),(((repeat ((Relax n) * (findmin n))) . 0) . f),n) = Argmin ((OuterVx (f,n)),(((repeat ((Relax n) * (findmin n))) . 0) . f),n) by Th21
.= 1 by A6, Th21 ;
thus UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) = UsedVx ((((repeat ((Relax n) * (findmin n))) . (0 + 1)) . f),n)
.= (UsedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n)) \/ {1} by A11, A12, Th39
.= (UsedVx (f,n)) \/ {1} by Th21
.= {1} by A9 ; :: thesis: verum