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 )

proof

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;

assume A4: 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: 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