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 v2 = (F _V) . v1 & F is isomorphism holds
(F _V) .: (G1 .reachableFrom v1) = G2 .reachableFrom v2
let F be 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) .: (G1 .reachableFrom v1) = G2 .reachableFrom v2
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v2 = (F _V) . v1 & F is isomorphism holds
(F _V) .: (G1 .reachableFrom v1) = G2 .reachableFrom v2
let v2 be Vertex of G2; :: thesis: ( v2 = (F _V) . v1 & F is isomorphism implies (F _V) .: (G1 .reachableFrom v1) = G2 .reachableFrom v2 )
assume A1: ( v2 = (F _V) . v1 & F is isomorphism ) ; :: thesis: (F _V) .: (G1 .reachableFrom v1) = G2 .reachableFrom v2
then A2: (F _V) .: (G1 .reachableFrom v1) c= G2 .reachableFrom v2 by Th80;
the_Vertices_of G1 = dom (F _V) by A1, GLIB_010:def 11;
then G2 .reachableFrom v2 c= (F _V) .: (G1 .reachableFrom v1) by A1, Th81;
hence (F _V) .: (G1 .reachableFrom v1) = G2 .reachableFrom v2 by A2, XBOOLE_0:def 10; :: thesis: verum