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