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 A1: ( 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 ) ) ; :: thesis: ( 1 = Argmin (OuterVx f,n),f,n & UsedVx f,n = {} & {1} = UsedVx (((repeat ((Relax n) * (findmin n))) . 1) . f),n )
A2: OuterVx f,n <> {}

proof

f . 1 = 1 by A1;
then 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;
hence OuterVx f,n <> {} ; :: thesis: verum

end;

set k = Argmin (OuterVx f,n),f,n;
thus A3: Argmin (OuterVx f,n),f,n = 1 :: thesis: ( UsedVx f,n = {} & {1} = UsedVx (((repeat ((Relax n) * (findmin n))) . 1) . f),n )

proof

assume A4: Argmin (OuterVx f,n),f,n <> 1 ; :: thesis: contradiction
A5: ( 1 <= Argmin (OuterVx f,n),f,n & Argmin (OuterVx f,n),f,n <= n & f . (Argmin (OuterVx f,n),f,n) <> - 1 & f . (n + (Argmin (OuterVx f,n),f,n)) <> - 1 ) by A2, Th30;
then 1 < Argmin (OuterVx f,n),f,n by A4, XXREAL_0:1;
then 1 + 1 <= Argmin (OuterVx f,n),f,n by INT_1:20;
hence contradiction by A1, A5; :: thesis: verum

end;

thus A6: 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
A7: x in UsedVx f,n by XBOOLE_0:def 1;
consider j being Element of NAT such that
A8: ( x = j & j in dom f & 1 <= j & j <= n & f . j = - 1 ) by A7;
thus contradiction by A1, A8; :: thesis: verum

end;

A9: OuterVx (((repeat ((Relax n) * (findmin n))) . 0 ) . f),n <> {} by A2, Th22;
A10: 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 A3, 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 A9, A10, Th40
.= (UsedVx f,n) \/ {1} by Th22
.= {1} by A6 ; :: thesis: verum