let G1, G2 be _Graph; :: thesis: for F being one-to-one PGraphMapping of G1,G2
for v1 being Vertex of G1
for v2 being Vertex of G2 st v2 = (F _V) . v1 & F is isomorphism holds
(F _V) " (G2 .reachableFrom v2) = G1 .reachableFrom v1
let F be one-to-one PGraphMapping of G1,G2; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v2 = (F _V) . v1 & F is isomorphism holds
(F _V) " (G2 .reachableFrom v2) = G1 .reachableFrom v1
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v2 = (F _V) . v1 & F is isomorphism holds
(F _V) " (G2 .reachableFrom v2) = G1 .reachableFrom v1
let v2 be Vertex of G2; :: thesis: ( v2 = (F _V) . v1 & F is isomorphism implies (F _V) " (G2 .reachableFrom v2) = G1 .reachableFrom v1 )
assume A1: ( v2 = (F _V) . v1 & F is isomorphism ) ; :: thesis: (F _V) " (G2 .reachableFrom v2) = G1 .reachableFrom v1
then the_Vertices_of G1 = dom (F _V) by GLIB_010:def 11;
then A2: ((F ") _V) . v2 = v1 by A1, FUNCT_1:34;
thus (F _V) " (G2 .reachableFrom v2) = ((F _V) ") .: (G2 .reachableFrom v2) by FUNCT_1:85
.= G1 .reachableFrom v1 by A1, A2, Th82, GLIB_010:75 ; :: thesis: verum