let G be _Graph; :: thesis: for W1 being Walk of G

for W2 being Subwalk of W1

for W3 being Subwalk of W2 holds W3 is Subwalk of W1

let W1 be Walk of G; :: thesis: for W2 being Subwalk of W1

for W3 being Subwalk of W2 holds W3 is Subwalk of W1

let W2 be Subwalk of W1; :: thesis: for W3 being Subwalk of W2 holds W3 is Subwalk of W1

let W3 be Subwalk of W2; :: thesis: W3 is Subwalk of W1

set fs = W1 .edgeSeq() ;

set fs1 = W2 .edgeSeq() ;

set fs2 = W3 .edgeSeq() ;

consider fss1 being Subset of (W2 .edgeSeq()) such that

A1: W3 .edgeSeq() = Seq fss1 by Def32;

consider fss being Subset of (W1 .edgeSeq()) such that

A2: W2 .edgeSeq() = Seq fss by Def32;

set fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1)));

reconsider fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) as Subset of (W1 .edgeSeq()) by FINSEQ_6:153;

A3: W3 .edgeSeq() = Seq fss2 by A1, A2, FINSEQ_6:154;

A4: W2 is_Walk_from W1 .first() ,W1 .last() by Def32;

then A5: W2 .last() = W1 .last() ;

W2 .first() = W1 .first() by A4;

hence W3 is Subwalk of W1 by A5, A3, Def32; :: thesis: verum

for W2 being Subwalk of W1

for W3 being Subwalk of W2 holds W3 is Subwalk of W1

let W1 be Walk of G; :: thesis: for W2 being Subwalk of W1

for W3 being Subwalk of W2 holds W3 is Subwalk of W1

let W2 be Subwalk of W1; :: thesis: for W3 being Subwalk of W2 holds W3 is Subwalk of W1

let W3 be Subwalk of W2; :: thesis: W3 is Subwalk of W1

set fs = W1 .edgeSeq() ;

set fs1 = W2 .edgeSeq() ;

set fs2 = W3 .edgeSeq() ;

consider fss1 being Subset of (W2 .edgeSeq()) such that

A1: W3 .edgeSeq() = Seq fss1 by Def32;

consider fss being Subset of (W1 .edgeSeq()) such that

A2: W2 .edgeSeq() = Seq fss by Def32;

set fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1)));

reconsider fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) as Subset of (W1 .edgeSeq()) by FINSEQ_6:153;

A3: W3 .edgeSeq() = Seq fss2 by A1, A2, FINSEQ_6:154;

A4: W2 is_Walk_from W1 .first() ,W1 .last() by Def32;

then A5: W2 .last() = W1 .last() ;

W2 .first() = W1 .first() by A4;

hence W3 is Subwalk of W1 by A5, A3, Def32; :: thesis: verum