set e = choose (Edges_At v,X);
set IT = { c where c is Element of X * : ( c is Path of & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;

A2: now

let x be set ; :: thesis: ( x in { c where c is Element of X * : ( c is Path of & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } implies x is FinSequence of the carrier' of G )
assume x in { c where c is Element of X * : ( c is Path of & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } ; :: thesis: x is FinSequence of the carrier' of G
then ex c being Element of X * st
( x = c & c is Path of & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) ;
hence x is FinSequence of the carrier' of G ; :: thesis: verum

end;

A3: not Edges_At v,X is empty by A1, Th30;

now

per cases ( choose (Edges_At v,X) in Edges_In v,X or choose (Edges_At v,X) in Edges_Out v,X ) by A3, XBOOLE_0:def 3;

suppose A4: choose (Edges_At v,X) in Edges_In v,X ; :: thesis: ex e' being Element of X st
( choose (Edges_At v,X) = e' & e' in X & e' in the carrier' of G & ( v = the Target of G . e' or v = the Source of G . e' ) )

then ( choose (Edges_At v,X) in X & the Target of G . (choose (Edges_At v,X)) = v ) by Def1;
hence ex e' being Element of X st
( choose (Edges_At v,X) = e' & e' in X & e' in the carrier' of G & ( v = the Target of G . e' or v = the Source of G . e' ) ) by A4; :: thesis: verum

end;

suppose A5: choose (Edges_At v,X) in Edges_Out v,X ; :: thesis: ex e' being Element of X st
( choose (Edges_At v,X) = e' & e' in X & e' in the carrier' of G & ( v = the Target of G . e' or v = the Source of G . e' ) )

then ( choose (Edges_At v,X) in X & the Source of G . (choose (Edges_At v,X)) = v ) by Def2;
hence ex e' being Element of X st
( choose (Edges_At v,X) = e' & e' in X & e' in the carrier' of G & ( v = the Target of G . e' or v = the Source of G . e' ) ) by A5; :: thesis: verum

end;

end;

end;

then consider e' being Element of X such that
choose (Edges_At v,X) = e' and
A6: e' in X and
A7: e' in the carrier' of G and
A8: ( v = the Target of G . e' or v = the Source of G . e' ) ;
reconsider X' = X as non empty set by A6;
reconsider e' = e' as Element of X' ;
reconsider c = <*e'*> as Element of X * by FINSEQ_1:def 11;
A9: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v )

proof

set s = the Source of G . e';
reconsider s = the Source of G . e' as Vertex of G by A7, FUNCT_2:7;
set t = the Target of G . e';
reconsider t = the Target of G . e' as Vertex of G by A7, FUNCT_2:7;

per cases ( v = the Target of G . e' or v = the Source of G . e' ) by A8;

suppose A10: v = the Target of G . e' ; :: thesis: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v )

take <*t,s*> ; :: thesis: ( <*t,s*> is_vertex_seq_of c & <*t,s*> . 1 = v )
thus ( <*t,s*> is_vertex_seq_of c & <*t,s*> . 1 = v ) by A10, Th16, FINSEQ_1:61; :: thesis: verum

end;

suppose A11: v = the Source of G . e' ; :: thesis: ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v )

take <*s,t*> ; :: thesis: ( <*s,t*> is_vertex_seq_of c & <*s,t*> . 1 = v )
thus ( <*s,t*> is_vertex_seq_of c & <*s,t*> . 1 = v ) by A11, FINSEQ_1:61, MSSCYC_1:4; :: thesis: verum

end;

end;

end;

c is Path of by A7, Th7;
then c in { c where c is Element of X * : ( c is Path of & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } by A9;
hence { c where c is Element of X * : ( c is Path of & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } is FinSequence-DOMAIN of by A2, FINSEQ_2:def 3; :: thesis: verum