let G1, G2 be _Graph; :: thesis:
let F be PGraphMapping of G1,G2; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: ( v1 in dom (F _V) & v2 = (F _V) . v1 & F is one-to-one & F is onto ) ; :: thesis:
then reconsider F0 = F as non empty one-to-one PGraphMapping of G1,G2 ;
A2: ((F0 ") _V) . v2 = v1 by A1, FUNCT_1:34;

now :: thesis:

let y be object ; :: thesis:
assume y in G2 .reachableFrom v2 ; :: thesis:
then consider W2 being Walk of G2 such that
A3: W2 is_Walk_from v2,y by GLIB_002:def 5;
W2 is F0 -valued by A1, GLIB_010:122;
then reconsider W2 = W2 as F0 " -defined Walk of G2 ;
(F0 ") .: W2 is_Walk_from ((F0 ") _V) . v2,((F0 ") _V) . y by A3, GLIB_010:132;
then A4: ((F0 ") _V) . y in G1 .reachableFrom v1 by A2, GLIB_002:def 5;
( y is Vertex of G2 & rng (F _V) = the_Vertices_of G2 ) by A1, A3, GLIB_001:18, GLIB_010:def 12;
then ( ((F0 _V) ") . y in dom (F _V) & y = (F0 _V) . (((F0 _V) ") . y) ) by FUNCT_1:32;
hence y in (F _V) .: (G1 .reachableFrom v1) by A4, FUNCT_1:def 6; :: thesis:

end;

hence G2 .reachableFrom v2 c= (F _V) .: (G1 .reachableFrom v1) by TARSKI:def 3; :: thesis: