let G be non void Graph; :: thesis: for oc being non empty directed Chain of G
for n being Nat st 1 <= n & n <= len oc holds
( (vertex-seq oc) . n = the Source of G . (oc . n) & (vertex-seq oc) . (n + 1) = the Target of G . (oc . n) )
let oc be non empty directed Chain of G; :: thesis: for n being Nat st 1 <= n & n <= len oc holds
( (vertex-seq oc) . n = the Source of G . (oc . n) & (vertex-seq oc) . (n + 1) = the Target of G . (oc . n) )
set vsoc = vertex-seq oc;
set S = the Source of G;
set T = the Target of G;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len oc implies ( (vertex-seq oc) . $1 = the Source of G . (oc . $1) & (vertex-seq oc) . ($1 + 1) = the Target of G . (oc . $1) ) );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: ( 1 <= n & n <= len oc implies ( (vertex-seq oc) . n = the Source of G . (oc . n) & (vertex-seq oc) . (n + 1) = the Target of G . (oc . n) ) ) ; :: thesis: S₁[n + 1]
A3: vertex-seq oc is_vertex_seq_of oc by GRAPH_2:def 10;
assume that
A4: 1 <= n + 1 and
A5: n + 1 <= len oc ; :: thesis: ( (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) & (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) )

per cases ( n = 0 or n <> 0 ) ;

suppose A6: n = 0 ; :: thesis: ( (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) & (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) )

hence A7: (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) by GRAPH_2:def 10; :: thesis: (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1))
1 in dom (vertex-seq oc) by FINSEQ_5:6;
then A8: (vertex-seq oc) /. 1 = (vertex-seq oc) . 1 by PARTFUN1:def 6;
A9: 1 <= len oc by A4, A5, XXREAL_0:2;
len (vertex-seq oc) = (len oc) + 1 by Th9;
then 1 + 1 <= len (vertex-seq oc) by A9, XREAL_1:6;
then 1 + 1 in dom (vertex-seq oc) by FINSEQ_3:25;
then A10: (vertex-seq oc) /. (1 + 1) = (vertex-seq oc) . (1 + 1) by PARTFUN1:def 6;
oc . 1 joins (vertex-seq oc) /. 1,(vertex-seq oc) /. (1 + 1) by A3, A9;
hence (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) by A6, A7, A8, A10; :: thesis: verum

end;

suppose A11: n <> 0 ; :: thesis: ( (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) & (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) )

A12: n < len oc by A5, NAT_1:13;
1 <= n by A11, NAT_1:14;
hence A13: (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) by A2, A12, GRAPH_1:def 15; :: thesis: (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1))
A14: len (vertex-seq oc) = (len oc) + 1 by Th9;
then ( 1 <= (n + 1) + 1 & (n + 1) + 1 <= len (vertex-seq oc) ) by A5, NAT_1:11, XREAL_1:6;
then (n + 1) + 1 in dom (vertex-seq oc) by FINSEQ_3:25;
then A15: (vertex-seq oc) /. ((n + 1) + 1) = (vertex-seq oc) . ((n + 1) + 1) by PARTFUN1:def 6;
n <= n + 1 by NAT_1:11;
then n <= len oc by A5, XXREAL_0:2;
then n + 1 <= len (vertex-seq oc) by A14, XREAL_1:6;
then n + 1 in dom (vertex-seq oc) by A4, FINSEQ_3:25;
then A16: (vertex-seq oc) /. (n + 1) = (vertex-seq oc) . (n + 1) by PARTFUN1:def 6;
oc . (n + 1) joins (vertex-seq oc) /. (n + 1),(vertex-seq oc) /. ((n + 1) + 1) by A4, A5, A3;
hence (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) by A13, A16, A15; :: thesis: verum

end;

end;

end;

A17: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A17, A1); :: thesis: verum