let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 in dom (F _V) & v2 = (F _V) . v1 & F is one-to-one & F is onto holds
G2 .reachableFrom v2 c= (F _V) .: (G1 .reachableFrom v1)
let F be PGraphMapping of G1,G2; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 in dom (F _V) & v2 = (F _V) . v1 & F is one-to-one & F is onto holds
G2 .reachableFrom v2 c= (F _V) .: (G1 .reachableFrom v1)
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 in dom (F _V) & v2 = (F _V) . v1 & F is one-to-one & F is onto holds
G2 .reachableFrom v2 c= (F _V) .: (G1 .reachableFrom v1)
let v2 be Vertex of G2; :: thesis: ( v1 in dom (F _V) & v2 = (F _V) . v1 & F is one-to-one & F is onto implies G2 .reachableFrom v2 c= (F _V) .: (G1 .reachableFrom v1) )
assume A1: ( v1 in dom (F _V) & v2 = (F _V) . v1 & F is one-to-one & F is onto ) ; :: thesis: G2 .reachableFrom v2 c= (F _V) .: (G1 .reachableFrom v1)
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: for y being object st y in G2 .reachableFrom v2 holds
y in (F _V) .: (G1 .reachableFrom v1)

let y be object ; :: thesis: ( y in G2 .reachableFrom v2 implies y in (F _V) .: (G1 .reachableFrom v1) )
assume y in G2 .reachableFrom v2 ; :: thesis: y in (F _V) .: (G1 .reachableFrom v1)
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: verum

end;

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