let n be 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 q9 = q | (Seg n) as FinSequence ;
for i being Nat st 1 <= i & i < len q9 holds
the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i)

proof

let i be Nat; :: thesis: ( 1 <= i & i < len q9 implies the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) )
assume that
A1: 1 <= i and
A2: i < len q9 ; :: 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:49;
hence the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) by A1, A2, GRAPH_1:def 15; :: thesis: verum

end;

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

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

end;

end;

end;

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