let S be vertex-disjoint GraphUnionSet; :: thesis: for G being GraphUnion of S
for H being Element of S
for v being Vertex of G
for w being Vertex of H st v = w holds
G .reachableFrom v = H .reachableFrom w
let G be GraphUnion of S; :: thesis: for H being Element of S
for v being Vertex of G
for w being Vertex of H st v = w holds
G .reachableFrom v = H .reachableFrom w
let H be Element of S; :: thesis: for v being Vertex of G
for w being Vertex of H st v = w holds
G .reachableFrom v = H .reachableFrom w
let v be Vertex of G; :: thesis: for w being Vertex of H st v = w holds
G .reachableFrom v = H .reachableFrom w
let w be Vertex of H; :: thesis: ( v = w implies G .reachableFrom v = H .reachableFrom w )
assume A1: v = w ; :: thesis: G .reachableFrom v = H .reachableFrom w
H is Subgraph of G by GLIB_014:21;
then A2: H .reachableFrom w c= G .reachableFrom v by A1, GLIB_002:14;
now :: thesis: for x being object st x in G .reachableFrom v holds
x in H .reachableFrom w
let x be object ; :: thesis: ( x in G .reachableFrom v implies x in H .reachableFrom w )
assume x in G .reachableFrom v ; :: thesis: x in H .reachableFrom w
then consider W being Walk of G such that
A3: W is_Walk_from v,x by GLIB_002:def 5;
consider H9 being Element of S such that
A4: W is Walk of H9 by Th58;
reconsider W9 = W as Walk of H9 by A4;
A5: W9 is_Walk_from v,x by A3, GLIB_001:19;
then ( v is Vertex of H9 & x is Vertex of H9 ) by GLIB_001:18;
then the_Vertices_of H meets the_Vertices_of H9 by A1, XBOOLE_0:3;
then reconsider W0 = W9 as Walk of H by Def18;
W0 is_Walk_from w,x by A1, A5, GLIB_001:19;
hence x in H .reachableFrom w by GLIB_002:def 5; :: thesis: verum
end;
then G .reachableFrom v c= H .reachableFrom w by TARSKI:def 3;
hence G .reachableFrom v = H .reachableFrom w by A2, XBOOLE_0:def 10; :: thesis: verum