let p be FinSequence; :: thesis: for n being Element of NAT
for G being Graph st p is OrientedPath of G holds
p | (Seg n) is OrientedPath of G
let n be Element of NAT ; :: thesis: for G being Graph st p is OrientedPath of G holds
p | (Seg n) is OrientedPath of G
let G be Graph; :: thesis: ( p is OrientedPath of G implies p | (Seg n) is OrientedPath of G )
assume A1: p is OrientedPath of G ; :: thesis: p | (Seg n) is OrientedPath of G
then reconsider p' = p | (Seg n) as oriented Chain of G by Th18;
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:19;

now

let n1, m1 be Element of NAT ; :: thesis: ( 1 <= n1 & n1 < m1 & m1 <= len q implies q . n1 <> q . m1 )
assume A2: ( 1 <= n1 & n1 < m1 & m1 <= len q ) ; :: thesis: q . n1 <> q . m1
then 1 < m1 by XXREAL_0:2;
then m1 in dom q by A2, FINSEQ_3:27;
then A3: q . m1 = p . m1 by FUNCT_1:70;
n1 < len q by A2, XXREAL_0:2;
then n1 in dom q by A2, FINSEQ_3:27;
then A4: q . n1 = p . n1 by FUNCT_1:70;
dom q c= dom p by RELAT_1:89;
then dom q c= Seg (len p) by FINSEQ_1:def 3;
then Seg (len q) c= Seg (len p) by FINSEQ_1:def 3;
then len q <= len p by FINSEQ_1:7;
then m1 <= len p by A2, XXREAL_0:2;
hence q . n1 <> q . m1 by A1, A2, A3, A4, GRAPH_1:def 14; :: thesis: verum

end;

then p' is Path of G by GRAPH_1:def 14;
hence p | (Seg n) is OrientedPath of G ; :: thesis: verum