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

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

hence
p | (Seg n) is Path of G
by A1, GRAPH_1:4, GRAPH_1:def 16; :: thesis: verumq . 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;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