let j, k, n be Nat; :: thesis: for f, g, h being Element of REAL *
for p being FinSequence of NAT st g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & len f = ((n * n) + (3 * n)) + 1 & p is_simple_vertex_seq_at g,j,n & g . (n + j) = h . (n + j) & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) holds
p is_simple_vertex_seq_at h,j,n
let f, g, h be Element of REAL * ; :: thesis: for p being FinSequence of NAT st g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & len f = ((n * n) + (3 * n)) + 1 & p is_simple_vertex_seq_at g,j,n & g . (n + j) = h . (n + j) & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) holds
p is_simple_vertex_seq_at h,j,n
let p be FinSequence of NAT ; :: thesis: ( g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & len f = ((n * n) + (3 * n)) + 1 & p is_simple_vertex_seq_at g,j,n & g . (n + j) = h . (n + j) & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) implies p is_simple_vertex_seq_at h,j,n )
set RT = repeat ((Relax n) * (findmin n));
assume that
A1: ( g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & len f = ((n * n) + (3 * n)) + 1 ) and
A2: p is_simple_vertex_seq_at g,j,n and
A3: g . (n + j) = h . (n + j) and
A4: for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ; :: thesis: p is_simple_vertex_seq_at h,j,n
A5: len p > 1 by A2;
A6: p is_vertex_seq_at g,j,n by A2;
then A7: p . (len p) = j ;

now :: thesis: for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = h . (n + (p /. (((len p) - k) + 1)))

let k be Nat; :: thesis: ( 1 <= k & k < len p implies p . ((len p) - b₁) = h . (n + (p /. (((len p) - b₁) + 1))) )
assume that
A8: 1 <= k and
A9: k < len p ; :: thesis: p . ((len p) - b₁) = h . (n + (p /. (((len p) - b₁) + 1)))
A10: k - k < (len p) - k by A9, XREAL_1:14;
then reconsider m = (len p) - k as Element of NAT by INT_1:3;
m <= (len p) - 1 by A8, XREAL_1:13;
then A11: m + 1 <= ((len p) - 1) + 1 by XREAL_1:7;
A12: 1 + 0 < m + 1 by A10, XREAL_1:8;
then A13: p /. (m + 1) = p . (m + 1) by A11, FINSEQ_4:15;

per cases ( m + 1 = len p or m + 1 <> len p ) ;

suppose m + 1 = len p ; :: thesis: p . ((len p) - b₁) = h . (n + (p /. (((len p) - b₁) + 1)))

hence p . ((len p) - k) = h . (n + (p /. (((len p) - k) + 1))) by A3, A5, A6, A13; :: thesis: verum

end;

suppose m + 1 <> len p ; :: thesis: p . ((len p) - b₁) = h . (n + (p /. (((len p) - b₁) + 1)))

then A14: m + 1 < len p by A11, XXREAL_0:1;
thus p . ((len p) - k) = g . (n + (p /. (((len p) - k) + 1))) by A6, A8, A9
.= h . (n + (p /. (((len p) - k) + 1))) by A1, A4, A12, A13, A14, Lm16 ; :: thesis: verum

end;

end;

end;

then A15: p is_vertex_seq_at h,j,n by A7;
( p . 1 = 1 & p is one-to-one ) by A2;
hence p is_simple_vertex_seq_at h,j,n by A5, A15; :: thesis: verum