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;

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

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

end;

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;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

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;

end;A21: len p > len q by A12, A19, XXREAL_0:1;

hereby :: thesis: verum
end;

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

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;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

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

p . k = q . k

hence
p = q
by A11, FINSEQ_1:14; :: thesis: verump . k = q . k

let k be Nat; :: thesis: ( 1 <= k & k <= len p implies p . b_{1} = q . b_{1} )

assume that

A27: 1 <= k and

A28: k <= len p ; :: thesis: p . b_{1} = q . b_{1}

end;assume that

A27: 1 <= k and

A28: k <= len p ; :: thesis: p . b

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

end;

suppose
k <> len p
; :: thesis: p . b_{1} = q . b_{1}

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;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