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 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 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
A8: p is_vertex_seq_at g,m,n by A2, Def18;
then A9: p . (len p) = m by Def17;
set q = p ^ <*j*>;
A10: len p > 1 by A2, Def18;
A11: len (p ^ <*j*>) = (len p) + 1 by FINSEQ_2:19;
then A12: (p ^ <*j*>) . (len (p ^ <*j*>)) = j by 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 that
A13: 1 <= ii and
A14: ii < len (p ^ <*j*>) ; :: thesis: (p ^ <*j*>) . ((len (p ^ <*j*>)) - b₁) = h . (n + ((p ^ <*j*>) /. (((len (p ^ <*j*>)) - b₁) + 1)))
A15: ii - ii < (len (p ^ <*j*>)) - ii by A14, XREAL_1:16;
then reconsider mm = (len (p ^ <*j*>)) - ii as Element of NAT by INT_1:16;
A16: 1 + 0 < mm + 1 by A15, XREAL_1:10;
mm <= (len (p ^ <*j*>)) - 1 by A13, XREAL_1:15;
then A17: mm + 1 <= ((len (p ^ <*j*>)) - 1) + 1 by XREAL_1:9;
then A18: (p ^ <*j*>) /. (mm + 1) = (p ^ <*j*>) . (mm + 1) by A16, 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 A3, A10, A9, A11, A12, A18, 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 A19: mm + 1 < len (p ^ <*j*>) by A17, XXREAL_0:1;
then A20: mm + 1 <= len p by A11, INT_1:20;
A21: 1 + 0 <= mm by A15, INT_1:20;
mm < len p by A11, A19, XREAL_1:9;
then A22: (p ^ <*j*>) . ((len (p ^ <*j*>)) - ii) = p . mm by A21, Lm1;

hereby :: thesis: verum

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

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

A24: p /. (((len p) - 1) + 1) = m by A10, A9, FINSEQ_4:24;
(p ^ <*j*>) /. (((len (p ^ <*j*>)) - ii) + 1) = m by A10, A9, A18, A23, Lm1;
hence (p ^ <*j*>) . ((len (p ^ <*j*>)) - ii) = h . (n + ((p ^ <*j*>) /. (((len (p ^ <*j*>)) - ii) + 1))) by A4, A10, A8, A22, A23, A24, Def17; :: thesis: verum

end;

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

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

A27: now

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

end;

then reconsider i3 = ii - 1 as Element of NAT by INT_1:16;
A28: p /. (mm + 1) = p . (mm + 1) by A16, A20, FINSEQ_4:24;
A29: (p ^ <*j*>) /. (((len (p ^ <*j*>)) - ii) + 1) = (p ^ <*j*>) . (mm + 1) by A16, A17, FINSEQ_4:24
.= p /. (mm + 1) by A16, A20, A28, Lm1 ;
ii - 1 < (len (p ^ <*j*>)) - 1 by A14, XREAL_1:16;
hence (p ^ <*j*>) . ((len (p ^ <*j*>)) - ii) = g . (n + (p /. (((len p) - i3) + 1))) by A8, A11, A22, A27, Def17
.= h . (n + ((p ^ <*j*>) /. (((len (p ^ <*j*>)) - ii) + 1))) by A1, A7, A11, A16, A26, A28, A29, Lm16 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

then A30: p ^ <*j*> is_vertex_seq_at h,j,n by A12, Def17;

A31: now

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

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

suppose i = len p ; :: thesis: contradiction

hence contradiction by A5, A8, A33, Def17; :: thesis: verum

end;

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

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

end;

end;

end;

p is one-to-one by A2, Def18;
then A36: p ^ <*j*> is one-to-one by A31, Th1;
p . 1 = 1 by A2, Def18;
then A37: (p ^ <*j*>) . 1 = 1 by A10, Lm1;
len (p ^ <*j*>) > 1 by A10, A11, NAT_1:13;
hence p ^ <*j*> is_simple_vertex_seq_at h,j,n by A37, A30, A36, Def18; :: thesis: verum