let p be FinSequence; :: thesis: for n being Nat
for G being Graph st p is Path of G holds
p | (Seg n) is Path of G

let n be Nat; :: thesis: for G being Graph st p is Path of G holds
p | (Seg n) is Path of G

let G be Graph; :: thesis: ( p is Path of G implies p | (Seg n) is Path of G )
reconsider q = p | (Seg n) as FinSequence ;
assume A1: p is Path of G ; :: thesis: p | (Seg n) is Path of G
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 ;
then m1 in dom q by ;
then A5: q . m1 = p . m1 by FUNCT_1:47;
n1 < len q by ;
then n1 in dom q by ;
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 ;
hence q . n1 <> q . m1 by ; :: thesis: verum
end;
hence p | (Seg n) is Path of G by ; :: thesis: verum