let n be Nat; 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; 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; 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; ( 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
; ( 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))
; vs1 is_oriented_vertex_seq_of c1
now ( 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
;
( 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;
for k being Nat st 1 <= k & k <= len c1 holds
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1)let k be
Nat;
( 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
;
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;
verum end; end; end;
hence
vs1 is_oriented_vertex_seq_of c1
; verum