let n be Nat; :: thesis: for G being Graph
for vs, vs1 being FinSequence of the carrier of G
for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds
vs1 is_oriented_vertex_seq_of c1
let G be Graph; :: thesis: for vs, vs1 being FinSequence of the carrier of G
for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds
vs1 is_oriented_vertex_seq_of c1
let vs, vs1 be FinSequence of the carrier of G; :: thesis: for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds
vs1 is_oriented_vertex_seq_of c1
let c, c1 be oriented Chain of G; :: thesis: ( vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) implies vs1 is_oriented_vertex_seq_of c1 )
assume A1: vs is_oriented_vertex_seq_of c ; :: thesis: ( not c1 = c | (Seg n) or not vs1 = vs | (Seg (n + 1)) or vs1 is_oriented_vertex_seq_of c1 )
then A2: len vs = (len c) + 1 ;
assume that
A3: c1 = c | (Seg n) and
A4: vs1 = vs | (Seg (n + 1)) ; :: thesis: vs1 is_oriented_vertex_seq_of c1
now :: thesis: ( len vs1 = (len c1) + 1 & ( for k being Nat st 1 <= k & k <= len c1 holds
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) )
per cases ( n <= len c or len c <= n ) ;
suppose A5: n <= len c ; :: thesis: ( len vs1 = (len c1) + 1 & ( for k being Nat st 1 <= k & k <= len c1 holds
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) )
then A6: n + 1 <= len vs by A2, XREAL_1:6;
A7: len c1 = n by A3, A5, FINSEQ_1:17;
A8: len vs1 = n + 1 by A4, A6, FINSEQ_1:17;
thus len vs1 = (len c1) + 1 by A4, A6, A7, FINSEQ_1:17; :: thesis: for k being Nat st 1 <= k & k <= len c1 holds
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1)
let k be Nat; :: thesis: ( 1 <= k & k <= len c1 implies c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) )
assume that
A9: 1 <= k and
A10: k <= len c1 ; :: thesis: c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1)
A11: k <= len c by A5, A7, A10, XXREAL_0:2;
k in Seg n by A7, A9, A10, FINSEQ_1:1;
then A12: c1 . k = c . k by A3, FUNCT_1:49;
A13: k <= len vs by A2, A11, NAT_1:12;
A14: k <= n + 1 by A7, A10, NAT_1:12;
then A15: k in Seg (n + 1) by A9, FINSEQ_1:1;
A16: 1 <= k + 1 by NAT_1:12;
k + 1 <= (len c1) + 1 by A10, XREAL_1:7;
then A17: k + 1 in Seg (n + 1) by A7, A16, FINSEQ_1:1;
A18: vs1 . k = vs . k by A4, A15, FUNCT_1:49;
A19: vs1 . (k + 1) = vs . (k + 1) by A4, A17, FUNCT_1:49;
A20: vs /. k = vs . k by A9, A13, FINSEQ_4:15;
A21: vs /. (k + 1) = vs . (k + 1) by A2, A11, A16, FINSEQ_4:15, XREAL_1:7;
A22: vs1 /. k = vs1 . k by A8, A9, A14, FINSEQ_4:15;
vs1 /. (k + 1) = vs1 . (k + 1) by A7, A8, A10, A16, FINSEQ_4:15, XREAL_1:7;
hence c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) by A1, A9, A11, A12, A18, A19, A20, A21, A22; :: thesis: verum
end;
suppose A23: len c <= n ; :: thesis: ( len vs1 = (len c1) + 1 & ( for k being Nat st 1 <= k & k <= len c1 holds
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) )
then A24: len vs <= n + 1 by A2, XREAL_1:6;
A25: c1 = c by A3, A23, FINSEQ_2:20;
vs1 = vs by A4, A24, FINSEQ_2:20;
hence ( len vs1 = (len c1) + 1 & ( for k being Nat st 1 <= k & k <= len c1 holds
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) ) by A1, A25; :: thesis: verum
end;
end;
end;
hence vs1 is_oriented_vertex_seq_of c1 ; :: thesis: verum