let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 holds

( F is directed iff for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) )

let F be PGraphMapping of G1,G2; :: thesis: ( F is directed iff for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) )

thus ( F is directed implies for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) ) :: thesis: ( ( for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) ) implies F is directed )

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) ; :: thesis: F is directed

let e, v, w be object ; :: according to GLIB_010:def 14 :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 implies (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 )

assume A5: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( not e DJoins v,w,G1 or (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 )

assume e DJoins v,w,G1 ; :: thesis: (F _E) . e DJoins (F _V) . v,(F _V) . w,G2

then A6: ( (the_Source_of G1) . e = v & (the_Target_of G1) . e = w ) by GLIB_000:def 14;

( (the_Source_of G2) . ((F _E) . e) = (F _V) . v & (the_Target_of G2) . ((F _E) . e) = (F _V) . w ) by A4, A5, A6;

hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A5, PARTFUN1:4, GLIB_000:def 14; :: thesis: verum

( F is directed iff for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) )

let F be PGraphMapping of G1,G2; :: thesis: ( F is directed iff for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) )

thus ( F is directed implies for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) ) :: thesis: ( ( for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) ) implies F is directed )

proof

assume A4:
for e being object st e in dom (F _E) holds
assume A1:
F is directed
; :: thesis: for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) )

let e be object ; :: thesis: ( e in dom (F _E) implies ( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) )

assume A2: e in dom (F _E) ; :: thesis: ( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) )

then A3: ( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) ) by Th5;

e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A2, GLIB_000:def 14;

then (F _E) . e DJoins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Target_of G1) . e),G2 by A1, A2, A3;

hence ( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) by GLIB_000:def 14; :: thesis: verum

end;( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) )

let e be object ; :: thesis: ( e in dom (F _E) implies ( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) )

assume A2: e in dom (F _E) ; :: thesis: ( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) )

then A3: ( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) ) by Th5;

e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A2, GLIB_000:def 14;

then (F _E) . e DJoins (F _V) . ((the_Source_of G1) . e),(F _V) . ((the_Target_of G1) . e),G2 by A1, A2, A3;

hence ( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) by GLIB_000:def 14; :: thesis: verum

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) ; :: thesis: F is directed

let e, v, w be object ; :: according to GLIB_010:def 14 :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 implies (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 )

assume A5: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( not e DJoins v,w,G1 or (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 )

assume e DJoins v,w,G1 ; :: thesis: (F _E) . e DJoins (F _V) . v,(F _V) . w,G2

then A6: ( (the_Source_of G1) . e = v & (the_Target_of G1) . e = w ) by GLIB_000:def 14;

( (the_Source_of G2) . ((F _E) . e) = (F _V) . v & (the_Target_of G2) . ((F _E) . e) = (F _V) . w ) by A4, A5, A6;

hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A5, PARTFUN1:4, GLIB_000:def 14; :: thesis: verum