let n, k, i be Element of NAT ; :: thesis: for g, f, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & i in UsedVx g,n & len f = ((n * n) + (3 * n)) + 1 holds
h . (n + i) = g . (n + i)
let g, f, h be Element of REAL * ; :: thesis: ( g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & i in UsedVx g,n & len f = ((n * n) + (3 * n)) + 1 implies h . (n + i) = g . (n + i) )
set R = Relax n;
set M = findmin n;
set RF = repeat ((Relax n) * (findmin n));
set mi = ((n * n) + (3 * n)) + 1;
set Ak = Argmin (OuterVx g,n),g,n;
assume that
A1: g = ((repeat ((Relax n) * (findmin n))) . k) . f and
A2: h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f and
A3: OuterVx g,n <> {} and
A4: i in UsedVx g,n and
A5: len f = ((n * n) + (3 * n)) + 1 ; :: thesis: h . (n + i) = g . (n + i)
A6: h = (Relax n) . ((findmin n) . g) by A1, A2, Th23
.= Relax ((findmin n) . g),n by Def15 ;
set ni = n + i;
A7: ex j being Element of NAT st
( i = j & j in dom g & 1 <= j & j <= n & g . j = - 1 ) by A4;
then A8: n + i <= n + n by XREAL_1:9;
A9: 1 <= n + i by A7, NAT_1:12;
A10: 2 * n < ((n * n) + (3 * n)) + 1 by Lm7;
then n + i < ((n * n) + (3 * n)) + 1 by A8, XXREAL_0:2;
then n + i in dom f by A5, A9, FINSEQ_3:27;
then n + i in dom g by A1, Th42;
then A11: ( (n + i) -' n = i & n + i in dom ((findmin n) . g) ) by Th34, NAT_D:34;
A12: Argmin (OuterVx g,n),g,n <= n by A3, Th30;
A13: n < ((n * n) + (3 * n)) + 1 by Lm7;
A14: (findmin n) . g = g,(((n * n) + (3 * n)) + 1) := (Argmin (OuterVx g,n),g,n),(- 1) by Def11;
A15: g . (Argmin (OuterVx g,n),g,n) <> - 1 by A3, Th30;

A16: now

assume (findmin n) . g hasBetterPathAt n,i ; :: thesis: contradiction
then ((findmin n) . g) . i <> - 1 by Def13;
hence contradiction by A14, A15, A7, A13, Th19; :: thesis: verum

end;

n + 1 <= n + i by A7, XREAL_1:9;
then A17: n < n + i by NAT_1:13;
n + i <= 2 * n by A8;
hence h . (n + i) = ((findmin n) . g) . (n + i) by A6, A17, A11, A16, Def14
.= g . (n + i) by A14, A12, A8, A17, A10, Th19 ;
:: thesis: verum