set e = choose (Edges_At (v,X));
set IT = { c where c is Element of X * : ( c is Path of G & 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 G & 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 G & 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 G & 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 e9 being Element of X st
( choose (Edges_At (v,X)) = e9 & e9 in X & e9 in the carrier' of G & ( v = the Target of G . e9 or v = the Source of G . e9 ) )

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

end;

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

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

end;

end;

end;

then consider e9 being Element of X such that
choose (Edges_At (v,X)) = e9 and
A6: e9 in X and
A7: e9 in the carrier' of G and
A8: ( v = the Target of G . e9 or v = the Source of G . e9 ) ;
reconsider X9 = X as non empty set by A6;
reconsider e9 = e9 as Element of X9 ;
reconsider c = <*e9*> 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 . e9;
reconsider s = the Source of G . e9 as Vertex of G by A7, FUNCT_2:5;
set t = the Target of G . e9;
reconsider t = the Target of G . e9 as Vertex of G by A7, FUNCT_2:5;

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

suppose A10: v = the Target of G . e9 ; :: 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:44; :: thesis: verum

end;

suppose A11: v = the Source of G . e9 ; :: 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:44, MSSCYC_1:4; :: thesis: verum

end;

end;

end;

c is Path of G by A7, Th7;
then c in { c where c is Element of X * : ( c is Path of G & 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 G & 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 the carrier' of G by A2, FINSEQ_2:def 3; :: thesis: verum