let n be Element of NAT ; :: thesis: for G being Graph
for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G
let G be Graph; :: thesis: for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G
let q be oriented Chain of G; :: thesis: q | (Seg n) is oriented Chain of G
reconsider q' = q | (Seg n) as FinSequence by FINSEQ_1:19;
for i being Element of NAT st 1 <= i & i < len q' holds
the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i)

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len q' implies the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) )
assume A1: ( 1 <= i & i < len q' ) ; :: thesis: the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i)

per cases ( n >= len q or n < len q ) ;

suppose n >= len q ; :: thesis: the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i)

then q | (Seg n) = q by FINSEQ_3:55;
hence the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) by A1, GRAPH_1:def 13; :: thesis: verum

end;

suppose A2: n < len q ; :: thesis: the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i)

then A3: len q' = n by FINSEQ_1:21;
then A4: i < len q by A1, A2, XXREAL_0:2;
i in Seg n by A1, A3, FINSEQ_1:3;
then A5: (q | (Seg n)) . i = q . i by FUNCT_1:72;
A6: i + 1 <= n by A1, A3, NAT_1:13;
1 < i + 1 by A1, NAT_1:13;
then i + 1 in Seg n by A6, FINSEQ_1:3;
then (q | (Seg n)) . (i + 1) = q . (i + 1) by FUNCT_1:72;
hence the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) by A1, A4, A5, GRAPH_1:def 13; :: thesis: verum

end;

end;

end;

hence q | (Seg n) is oriented Chain of G by GRAPH_1:4, GRAPH_1:def 13; :: thesis: verum