set v = the Element of dom (F _V);
reconsider v = the Element of dom (F _V) as Vertex of G1 ;
set W1 = G1 .walkOf v;
take G1 .walkOf v ; :: thesis: ( G1 .walkOf v is F -defined & G1 .walkOf v is V5() )
(G1 .walkOf v) .vertices() = {v} by GLIB_001:90;
hence (G1 .walkOf v) .vertices() c= dom (F _V) by ZFMISC_1:31; :: according to GLIB_010:def 35 :: thesis: ( (G1 .walkOf v) .edges() c= dom (F _E) & G1 .walkOf v is V5() )
thus (G1 .walkOf v) .edges() c= dom (F _E) by XBOOLE_1:2; :: thesis: G1 .walkOf v is V5()
thus G1 .walkOf v is V5() ; :: thesis: verum