let j, k, m, 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,m,n & m = h . (n + j) & g . (n + m) = h . (n + m) & m <> j & not j in UsedVx (g,n) & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) holds
for q being FinSequence of NAT st q = p ^ <*j*> holds
q 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,m,n & m = h . (n + j) & g . (n + m) = h . (n + m) & m <> j & not j in UsedVx (g,n) & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) holds
for q being FinSequence of NAT st q = p ^ <*j*> holds
q 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,m,n & m = h . (n + j) & g . (n + m) = h . (n + m) & m <> j & not j in UsedVx (g,n) & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) implies for q being FinSequence of NAT st q = p ^ <*j*> holds
q 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,m,n and
A3: m = h . (n + j) and
A4: g . (n + m) = h . (n + m) and
A5: m <> j and
A6: not j in UsedVx (g,n) and
A7: for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ; :: thesis: for q being FinSequence of NAT st q = p ^ <*j*> holds
q is_simple_vertex_seq_at h,j,n
A8: p is_vertex_seq_at g,m,n by A2;
then A9: p . (len p) = m ;
let q be FinSequence of NAT ; :: thesis: ( q = p ^ <*j*> implies q is_simple_vertex_seq_at h,j,n )
assume A10: q = p ^ <*j*> ; :: thesis: q is_simple_vertex_seq_at h,j,n
A11: len p > 1 by A2;
A12: len q = (len p) + 1 by FINSEQ_2:16, A10;
then A13: q . (len q) = j by FINSEQ_1:42, A10;

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

let ii be Nat; :: thesis: ( 1 <= ii & ii < len q implies q . ((len q) - b₁) = h . (n + (q /. (((len q) - b₁) + 1))) )
assume that
A14: 1 <= ii and
A15: ii < len q ; :: thesis: q . ((len q) - b₁) = h . (n + (q /. (((len q) - b₁) + 1)))
A16: ii - ii < (len q) - ii by A15, XREAL_1:14;
then reconsider mm = (len q) - ii as Element of NAT by INT_1:3;
A17: 1 + 0 < mm + 1 by A16, XREAL_1:8;
mm <= (len q) - 1 by A14, XREAL_1:13;
then A18: mm + 1 <= ((len q) - 1) + 1 by XREAL_1:7;
then A19: q /. (mm + 1) = q . (mm + 1) by A17, FINSEQ_4:15;

per cases ( mm + 1 = len q or mm + 1 <> len q ) ;

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

hence q . ((len q) - ii) = h . (n + (q /. (((len q) - ii) + 1))) by A3, A11, A9, A12, A13, A19, Lm1, A10; :: thesis: verum

end;

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

then A20: mm + 1 < len q by A18, XXREAL_0:1;
then A21: mm + 1 <= len p by A12, INT_1:7;
A22: 1 + 0 <= mm by A16, INT_1:7;
mm < len p by A12, A20, XREAL_1:7;
then A23: q . ((len q) - ii) = p . mm by A22, Lm1, A10;

hereby :: thesis: verum

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

suppose A24: mm + 1 = len p ; :: thesis: q . ((len q) - ii) = h . (n + (q /. (((len q) - ii) + 1)))

A25: p /. (((len p) - 1) + 1) = m by A11, A9, FINSEQ_4:15;
q /. (((len q) - ii) + 1) = m by A11, A9, A19, A24, Lm1, A10;
hence q . ((len q) - ii) = h . (n + (q /. (((len q) - ii) + 1))) by A4, A11, A8, A23, A24, A25; :: thesis: verum

end;

suppose A26: mm + 1 <> len p ; :: thesis: q . ((len q) - ii) = h . (n + (q /. (((len q) - ii) + 1)))

set i2 = ii - 1;
A27: mm + 1 < len p by A21, A26, XXREAL_0:1;

A28: now :: thesis: not ii - 1 <= 1

assume ii - 1 <= 1 ; :: thesis: contradiction
then (len p) - 1 <= (len p) - (ii - 1) by XREAL_1:13;
hence contradiction by A12, A27, XREAL_1:20; :: thesis: verum

end;

then reconsider i3 = ii - 1 as Element of NAT by INT_1:3;
A29: p /. (mm + 1) = p . (mm + 1) by A17, A21, FINSEQ_4:15;
A30: q /. (((len q) - ii) + 1) = q . (mm + 1) by A17, A18, FINSEQ_4:15
.= p /. (mm + 1) by A17, A21, A29, Lm1, A10 ;
ii - 1 < (len q) - 1 by A15, XREAL_1:14;
hence q . ((len q) - ii) = g . (n + (p /. (((len p) - i3) + 1))) by A8, A12, A23, A28
.= h . (n + (q /. (((len q) - ii) + 1))) by A1, A7, A12, A17, A27, A29, A30, Lm16 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

then A31: q is_vertex_seq_at h,j,n by A13;

A32: now :: thesis: not j in rng p

assume j in rng p ; :: thesis: contradiction
then consider i being Nat such that
A33: i in dom p and
A34: j = p . i by FINSEQ_2:10;
A35: 1 <= i by A33, FINSEQ_3:25;
A36: i <= len p by A33, FINSEQ_3:25;

per cases ( i = len p or i <> len p ) ;

suppose i = len p ; :: thesis: contradiction

hence contradiction by A5, A8, A34; :: thesis: verum

end;

suppose i <> len p ; :: thesis: contradiction

then i < len p by A36, XXREAL_0:1;
hence contradiction by A6, A7, A34, A35; :: thesis: verum

end;

end;

end;

p is one-to-one by A2;
then A37: q is one-to-one by A32, Th1, A10;
p . 1 = 1 by A2;
then A38: q . 1 = 1 by A11, Lm1, A10;
len q > 1 by A11, A12, NAT_1:13;
hence q is_simple_vertex_seq_at h,j,n by A38, A31, A37; :: thesis: verum