let n be Element of NAT ; :: thesis: for f being Element of REAL * st 1 <= n & 1 in dom f & f . (n + 1) <> - 1 & ( for i being Element of NAT st 1 <= i & i <= n holds
f . i = 1 ) & ( for i being Element of 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 Element of NAT st 1 <= i & i <= n holds
f . i = 1 ) & ( for i being Element of 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 Element of NAT st 1 <= i & i <= n holds
f . i = 1 and
A4: for i being Element of 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 Element of 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, Th30;
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:20;
( Argmin (OuterVx f,n),f,n <= n & f . (n + (Argmin (OuterVx f,n),f,n)) <> - 1 ) by A5, Th30;
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 set such that
A10: x in UsedVx f,n by XBOOLE_0:def 1;
ex j being Element of 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 Th22;
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 Th22
.= 1 by A6, Th22 ;
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, Th40
.= (UsedVx f,n) \/ {1} by Th22
.= {1} by A9 ; :: thesis: verum