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
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 . b1 = q . b1 )
assume that
A27: 1 <= k and
A28: k <= len p ; :: thesis: p . b1 = q . b1
per cases ( k = len p or k <> len p ) ;
suppose k = len p ; :: thesis: p . b1 = q . b1
hence p . k = q . k by A5, A8, A11; :: thesis: verum
end;
suppose k <> len p ; :: thesis: p . b1 = q . b1
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