let G1, G2 be _Graph; for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is directed & v in dom (F _V) holds
( (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() )
let F be PGraphMapping of G1,G2; for v being Vertex of G1 st F is directed & v in dom (F _V) holds
( (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() )
let v be Vertex of G1; ( F is directed & v in dom (F _V) implies ( (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() ) )
assume A1:
( F is directed & v in dom (F _V) )
; ( (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() )
now for e being object st e in (F _E) .: (v .edgesIn()) holds
e in ((F _V) /. v) .edgesIn() let e be
object ;
( e in (F _E) .: (v .edgesIn()) implies e in ((F _V) /. v) .edgesIn() )assume
e in (F _E) .: (v .edgesIn())
;
e in ((F _V) /. v) .edgesIn() then consider e0 being
object such that A2:
(
e0 in dom (F _E) &
e0 in v .edgesIn() &
e = (F _E) . e0 )
by FUNCT_1:def 6;
A3:
(the_Target_of G1) . e0 = v
by A2, GLIB_000:56;
set w =
(the_Source_of G1) . e0;
A4:
(the_Source_of G1) . e0 in dom (F _V)
by A2, GLIB_010:5;
e0 DJoins (the_Source_of G1) . e0,
v,
G1
by A2, A3, GLIB_000:def 14;
then
(F _E) . e0 DJoins (F _V) . ((the_Source_of G1) . e0),
(F _V) . v,
G2
by A1, A2, A4, GLIB_010:def 14;
then
(F _E) . e0 DJoins (F _V) . ((the_Source_of G1) . e0),
(F _V) /. v,
G2
by A1, PARTFUN1:def 6;
hence
e in ((F _V) /. v) .edgesIn()
by A2, GLIB_000:57;
verum end;
hence
(F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn()
by TARSKI:def 3; (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut()
now for e being object st e in (F _E) .: (v .edgesOut()) holds
e in ((F _V) /. v) .edgesOut() let e be
object ;
( e in (F _E) .: (v .edgesOut()) implies e in ((F _V) /. v) .edgesOut() )assume
e in (F _E) .: (v .edgesOut())
;
e in ((F _V) /. v) .edgesOut() then consider e0 being
object such that A5:
(
e0 in dom (F _E) &
e0 in v .edgesOut() &
e = (F _E) . e0 )
by FUNCT_1:def 6;
A6:
(the_Source_of G1) . e0 = v
by A5, GLIB_000:58;
set w =
(the_Target_of G1) . e0;
A7:
(the_Target_of G1) . e0 in dom (F _V)
by A5, GLIB_010:5;
e0 DJoins v,
(the_Target_of G1) . e0,
G1
by A5, A6, GLIB_000:def 14;
then
(F _E) . e0 DJoins (F _V) . v,
(F _V) . ((the_Target_of G1) . e0),
G2
by A1, A5, A7, GLIB_010:def 14;
then
(F _E) . e0 DJoins (F _V) /. v,
(F _V) . ((the_Target_of G1) . e0),
G2
by A1, PARTFUN1:def 6;
hence
e in ((F _V) /. v) .edgesOut()
by A5, GLIB_000:59;
verum end;
hence
(F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut()
by TARSKI:def 3; verum