let n, k, m, j be Element of NAT ; :: thesis: for g, f, 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 Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx g,n ) holds
p ^ <*j*> is_simple_vertex_seq_at h,j,n
let g, f, 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 Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx g,n ) holds
p ^ <*j*> 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 Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx g,n ) implies p ^ <*j*> is_simple_vertex_seq_at h,j,n )
set RT = repeat ((Relax n) * (findmin n));
assume 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 & 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 Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx g,n ) ) ; :: thesis: p ^ <*j*> is_simple_vertex_seq_at h,j,n
then A2: ( p . 1 = 1 & len p > 1 & p is_vertex_seq_at g,m,n & p is one-to-one ) by Def18;
then A3: p . (len p) = m by Def17;
set q = p ^ <*j*>;
A4: len (p ^ <*j*>) = (len p) + 1 by FINSEQ_2:19;
then A5: len (p ^ <*j*>) > 1 by A2, NAT_1:13;
A6: (p ^ <*j*>) . 1 = 1 by A2, Lm1;
A7: (p ^ <*j*>) . (len (p ^ <*j*>)) = j by A4, FINSEQ_1:59;

now

let ii be Element of NAT ; :: thesis: ( 1 <= ii & ii < len (p ^ <*j*>) implies (p ^ <*j*>) . ((len (p ^ <*j*>)) - b₁) = h . (n + ((p ^ <*j*>) /. (((len (p ^ <*j*>)) - b₁) + 1))) )
assume A8: ( 1 <= ii & ii < len (p ^ <*j*>) ) ; :: thesis: (p ^ <*j*>) . ((len (p ^ <*j*>)) - b₁) = h . (n + ((p ^ <*j*>) /. (((len (p ^ <*j*>)) - b₁) + 1)))
then A9: ii - ii < (len (p ^ <*j*>)) - ii by XREAL_1:16;
then reconsider mm = (len (p ^ <*j*>)) - ii as Element of NAT by INT_1:16;
A10: 1 + 0 < mm + 1 by A9, XREAL_1:10;
mm <= (len (p ^ <*j*>)) - 1 by A8, XREAL_1:15;
then A11: mm + 1 <= ((len (p ^ <*j*>)) - 1) + 1 by XREAL_1:9;
then A12: (p ^ <*j*>) /. (mm + 1) = (p ^ <*j*>) . (mm + 1) by A10, FINSEQ_4:24;

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

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

hence (p ^ <*j*>) . ((len (p ^ <*j*>)) - ii) = h . (n + ((p ^ <*j*>) /. (((len (p ^ <*j*>)) - ii) + 1))) by A1, A2, A3, A4, A7, A12, Lm1; :: thesis: verum

end;

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

then A13: mm + 1 < len (p ^ <*j*>) by A11, XXREAL_0:1;
then A14: mm < len p by A4, XREAL_1:9;
A15: mm + 1 <= len p by A4, A13, INT_1:20;
1 + 0 <= mm by A9, INT_1:20;
then A16: (p ^ <*j*>) . ((len (p ^ <*j*>)) - ii) = p . mm by A14, Lm1;

hereby :: thesis: verum

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

suppose A17: mm + 1 = len p ; :: thesis: (p ^ <*j*>) . ((len (p ^ <*j*>)) - ii) = h . (n + ((p ^ <*j*>) /. (((len (p ^ <*j*>)) - ii) + 1)))

A18: p /. (((len p) - 1) + 1) = m by A2, A3, FINSEQ_4:24;
(p ^ <*j*>) /. (((len (p ^ <*j*>)) - ii) + 1) = m by A2, A3, A12, A17, Lm1;
hence (p ^ <*j*>) . ((len (p ^ <*j*>)) - ii) = h . (n + ((p ^ <*j*>) /. (((len (p ^ <*j*>)) - ii) + 1))) by A1, A2, A16, A17, A18, Def17; :: thesis: verum

end;

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

then A19: mm + 1 < len p by A15, XXREAL_0:1;
A20: p /. (mm + 1) = p . (mm + 1) by A10, A15, FINSEQ_4:24;
set i2 = ii - 1;

A21: now

assume ii - 1 <= 1 ; :: thesis: contradiction
then (len p) - 1 <= (len p) - (ii - 1) by XREAL_1:15;
hence contradiction by A4, A19, XREAL_1:22; :: thesis: verum

end;

A22: (p ^ <*j*>) /. (((len (p ^ <*j*>)) - ii) + 1) = (p ^ <*j*>) . (mm + 1) by A10, A11, FINSEQ_4:24
.= p /. (mm + 1) by A10, A15, A20, Lm1 ;
reconsider i3 = ii - 1 as Element of NAT by A21, INT_1:16;
ii - 1 < (len (p ^ <*j*>)) - 1 by A8, XREAL_1:16;
hence (p ^ <*j*>) . ((len (p ^ <*j*>)) - ii) = g . (n + (p /. (((len p) - i3) + 1))) by A2, A4, A16, A21, Def17
.= h . (n + ((p ^ <*j*>) /. (((len (p ^ <*j*>)) - ii) + 1))) by A1, A4, A10, A19, A20, A22, Lm16 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

then A23: p ^ <*j*> is_vertex_seq_at h,j,n by A7, Def17;

now

assume j in rng p ; :: thesis: contradiction
then consider i being Nat such that
A24: ( i in dom p & j = p . i ) by FINSEQ_2:11;
A25: ( 1 <= i & i <= len p ) by A24, FINSEQ_3:27;

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

suppose i = len p ; :: thesis: contradiction

hence contradiction by A1, A2, A24, Def17; :: thesis: verum

end;

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

then i < len p by A25, XXREAL_0:1;
hence contradiction by A1, A24, A25; :: thesis: verum

end;

end;

end;

then p ^ <*j*> is one-to-one by A2, Th1;
hence p ^ <*j*> is_simple_vertex_seq_at h,j,n by A5, A6, A23, Def18; :: thesis: verum