let p, q be FinSequence of NAT ; :: thesis: for f being Element of REAL *
for i, n being Element of NAT st p is_simple_vertex_seq_at f,i,n & q is_simple_vertex_seq_at f,i,n holds
p = q
let f be Element of REAL * ; :: thesis: for i, n being Element of NAT st p is_simple_vertex_seq_at f,i,n & q is_simple_vertex_seq_at f,i,n holds
p = q
let i, n be Element of NAT ; :: thesis: ( p is_simple_vertex_seq_at f,i,n & q is_simple_vertex_seq_at f,i,n implies p = q )
assume that
A1: p is_simple_vertex_seq_at f,i,n and
A2: q is_simple_vertex_seq_at f,i,n ; :: thesis: p = q
A3: p . 1 = 1 by A1;
A4: q . 1 = 1 by A2;
A5: p is_vertex_seq_at f,i,n by A1;
then A6: ( p . (len p) = i & ( for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = f . ((p /. (((len p) - k) + 1)) + n) ) ) ;
A7: q is_vertex_seq_at f,i,n by A2;
then A8: q . (len q) = i ;
A9: for k being Nat st 1 <= k & k < len q holds
q . ((len q) - k) = f . ((q /. (((len q) - k) + 1)) + n) by A7;
A10: len p > 1 by A1;

A11: now :: thesis: not len p <> len q

assume A12: len p <> len q ; :: thesis: contradiction

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

suppose A13: len p < len q ; :: thesis: contradiction

A14: (len p) - 1 > 1 - 1 by A10, XREAL_1:14;
then reconsider k = (len p) - 1 as Element of NAT by INT_1:3;
A15: (len p) - k = 0 + 1 ;
then A16: (len q) - k > 1 by A13, XREAL_1:14;
then reconsider m = (len q) - k as Element of NAT by INT_1:3;
A17: k < len p by XREAL_1:146;
k >= 0 + 1 by A14, INT_1:7;
then A18: 1 = q . ((len q) - k) by A3, A6, A8, A9, A13, A15, A17, Lm10;
( q is one-to-one & m <= len q ) by A2, Lm9;
hence contradiction by A4, A18, A16, GRAPH_5:6; :: thesis: verum

end;

suppose A19: len p >= len q ; :: thesis: contradiction

A20: p is one-to-one by A1;
A21: len p > len q by A12, A19, XXREAL_0:1;

hereby :: thesis: verum

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

suppose len q <= 1 ; :: thesis: contradiction

hence contradiction by A2; :: thesis: verum

end;

suppose len q > 1 ; :: thesis: contradiction

then A22: (len q) - 1 > 1 - 1 by XREAL_1:14;
then reconsider k = (len q) - 1 as Element of NAT by INT_1:3;
A23: k < len q by XREAL_1:146;
A24: (len q) - k = 0 + 1 ;
then A25: (len p) - k > 1 by A21, XREAL_1:14;
then reconsider m = (len p) - k as Element of NAT by INT_1:3;
k >= 0 + 1 by A22, INT_1:7;
then A26: 1 = p . ((len p) - k) by A6, A4, A8, A9, A19, A24, A23, Lm10;
m <= len p by Lm9;
hence contradiction by A3, A20, A26, A25, GRAPH_5:6; :: thesis: verum

end;

end;

end;

end;

end;

end;

now :: thesis: for k being Nat st 1 <= k & k <= len p holds
p . k = q . k

let k be Nat; :: thesis: ( 1 <= k & k <= len p implies p . b₁ = q . b₁ )
assume that
A27: 1 <= k and
A28: k <= len p ; :: thesis: p . b₁ = q . b₁

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

suppose k = len p ; :: thesis: p . b₁ = q . b₁

hence p . k = q . k by A5, A8, A11; :: thesis: verum

end;

suppose k <> len p ; :: thesis: p . b₁ = q . b₁

then k < len p by A28, XXREAL_0:1;
then A29: (len p) - k > k - k by XREAL_1:14;
then reconsider m = (len p) - k as Element of NAT by INT_1:3;
A30: (len q) - m = 0 + k by A11;
(len p) - k <= (len p) - 1 by A27, XREAL_1:13;
then A31: m < len p by XREAL_1:146, XXREAL_0:2;
m >= 0 + 1 by A29, INT_1:7;
hence p . k = q . k by A6, A8, A9, A30, A31, Lm10; :: thesis: verum

end;

end;

end;

hence p = q by A11, FINSEQ_1:14; :: thesis: verum