let G be non void Graph; :: thesis: for oc being non empty directed Chain of G
for n being Element of 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 Element of 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₁[ Element of 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 Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let n be Element of 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 11;
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 11; :: thesis: (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1))
A8: ( (vertex-seq oc) /. 1 = (vertex-seq oc) /. (1 + 1) or (vertex-seq oc) /. 1 <> (vertex-seq oc) /. (1 + 1) ) ;
1 in dom (vertex-seq oc) by FINSEQ_5:6;
then A9: (vertex-seq oc) /. 1 = (vertex-seq oc) . 1 by PARTFUN1:def 8;
A10: 1 <= len oc by A4, A5, XXREAL_0:2;
len (vertex-seq oc) = (len oc) + 1 by Th10;
then 1 + 1 <= len (vertex-seq oc) by A10, XREAL_1:8;
then 1 + 1 in dom (vertex-seq oc) by FINSEQ_3:27;
then A11: (vertex-seq oc) /. (1 + 1) = (vertex-seq oc) . (1 + 1) by PARTFUN1:def 8;
oc . 1 joins (vertex-seq oc) /. 1,(vertex-seq oc) /. (1 + 1) by A3, A10, GRAPH_2:def 7;
hence (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) by A6, A7, A8, A9, A11, GRAPH_1:def 10; :: thesis: verum

end;

suppose A12: 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)) )

A13: n < len oc by A5, NAT_1:13;
1 <= n by A12, NAT_1:14;
hence A14: (vertex-seq oc) . (n + 1) = the Source of G . (oc . (n + 1)) by A2, A13, GRAPH_1:def 13; :: thesis: (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1))
A15: ( (vertex-seq oc) /. (n + 1) = (vertex-seq oc) /. ((n + 1) + 1) or (vertex-seq oc) /. (n + 1) <> (vertex-seq oc) /. ((n + 1) + 1) ) ;
A16: len (vertex-seq oc) = (len oc) + 1 by Th10;
then ( 1 <= (n + 1) + 1 & (n + 1) + 1 <= len (vertex-seq oc) ) by A5, NAT_1:11, XREAL_1:8;
then (n + 1) + 1 in dom (vertex-seq oc) by FINSEQ_3:27;
then A17: (vertex-seq oc) /. ((n + 1) + 1) = (vertex-seq oc) . ((n + 1) + 1) by PARTFUN1:def 8;
n <= n + 1 by NAT_1:11;
then n <= len oc by A5, XXREAL_0:2;
then n + 1 <= len (vertex-seq oc) by A16, XREAL_1:8;
then n + 1 in dom (vertex-seq oc) by A4, FINSEQ_3:27;
then A18: (vertex-seq oc) /. (n + 1) = (vertex-seq oc) . (n + 1) by PARTFUN1:def 8;
oc . (n + 1) joins (vertex-seq oc) /. (n + 1),(vertex-seq oc) /. ((n + 1) + 1) by A4, A5, A3, GRAPH_2:def 7;
hence (vertex-seq oc) . ((n + 1) + 1) = the Target of G . (oc . (n + 1)) by A14, A15, A18, A17, GRAPH_1:def 10; :: thesis: verum

end;

end;

end;

A19: S₁[ 0 ] ;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A19, A1); :: thesis: verum