let p be FinSequence; :: thesis: for n being Nat
for G being Graph st p is OrientedPath of G holds
p | (Seg n) is OrientedPath of G
let n be 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 p9 = p | (Seg n) as oriented Chain of G by Th16;
reconsider q = p | (Seg n) as FinSequence ;
now :: thesis: for n1, m1 being Nat st 1 <= n1 & n1 < m1 & m1 <= len q holds
q . n1 <> q . m1
let n1, m1 be Nat; :: thesis: ( 1 <= n1 & n1 < m1 & m1 <= len q implies q . n1 <> q . m1 )
assume that
A2: 1 <= n1 and
A3: n1 < m1 and
A4: m1 <= len q ; :: thesis: q . n1 <> q . m1
1 < m1 by A2, A3, XXREAL_0:2;
then m1 in dom q by A4, FINSEQ_3:25;
then A5: q . m1 = p . m1 by FUNCT_1:47;
n1 < len q by A3, A4, XXREAL_0:2;
then n1 in dom q by A2, FINSEQ_3:25;
then A6: q . n1 = p . n1 by FUNCT_1:47;
dom q c= dom p by RELAT_1:60;
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:5;
then m1 <= len p by A4, XXREAL_0:2;
hence q . n1 <> q . m1 by A1, A2, A3, A5, A6, GRAPH_1:def 16; :: thesis: verum
end;
then p9 is Path of G by GRAPH_1:def 16;
hence p | (Seg n) is OrientedPath of G ; :: thesis: verum