theorem Th47: :: GRAPHSP:47

for n being Nat
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) )