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 total holds
(F _V) .: (G1 .reachableFrom v1) c= 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 total holds
(F _V) .: (G1 .reachableFrom v1) c= G2 .reachableFrom v2
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v2 = (F _V) . v1 & F is total holds
(F _V) .: (G1 .reachableFrom v1) c= G2 .reachableFrom v2
let v2 be Vertex of G2; :: thesis: ( v2 = (F _V) . v1 & F is total implies (F _V) .: (G1 .reachableFrom v1) c= G2 .reachableFrom v2 )
assume A1: ( v2 = (F _V) . v1 & F is total ) ; :: thesis: (F _V) .: (G1 .reachableFrom v1) c= G2 .reachableFrom v2
then reconsider F0 = F as non empty PGraphMapping of G1,G2 ;
now :: thesis: for y being object st y in (F _V) .: (G1 .reachableFrom v1) holds
y in G2 .reachableFrom v2
let y be object ; :: thesis: ( y in (F _V) .: (G1 .reachableFrom v1) implies y in G2 .reachableFrom v2 )
assume y in (F _V) .: (G1 .reachableFrom v1) ; :: thesis: y in G2 .reachableFrom v2
then consider x being object such that
A2: ( x in dom (F _V) & x in G1 .reachableFrom v1 & y = (F _V) . x ) by FUNCT_1:def 6;
consider W1 being Walk of G1 such that
A3: W1 is_Walk_from v1,x by A2, GLIB_002:def 5;
reconsider W1 = W1 as F0 -defined Walk of G1 by A1, GLIB_010:121;
F0 .: W1 is_Walk_from (F0 _V) . v1,(F0 _V) . x by A3, GLIB_010:132;
hence y in G2 .reachableFrom v2 by A1, A2, GLIB_002:def 5; :: thesis: verum
end;
hence (F _V) .: (G1 .reachableFrom v1) c= G2 .reachableFrom v2 by TARSKI:def 3; :: thesis: verum