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
( () . ((F _E) . e) = (F _V) . (() . e) & () . ((F _E) . e) = (F _V) . (() . e) ) )

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

thus ( F is directed implies for e being object st e in dom (F _E) holds
( () . ((F _E) . e) = (F _V) . (() . e) & () . ((F _E) . e) = (F _V) . (() . e) ) ) :: thesis: ( ( for e being object st e in dom (F _E) holds
( () . ((F _E) . e) = (F _V) . (() . e) & () . ((F _E) . e) = (F _V) . (() . e) ) ) implies F is directed )
proof
assume A1: F is directed ; :: thesis: for e being object st e in dom (F _E) holds
( () . ((F _E) . e) = (F _V) . (() . e) & () . ((F _E) . e) = (F _V) . (() . e) )

let e be object ; :: thesis: ( e in dom (F _E) implies ( () . ((F _E) . e) = (F _V) . (() . e) & () . ((F _E) . e) = (F _V) . (() . e) ) )
assume A2: e in dom (F _E) ; :: thesis: ( () . ((F _E) . e) = (F _V) . (() . e) & () . ((F _E) . e) = (F _V) . (() . e) )
then A3: ( (the_Source_of G1) . e in dom (F _V) & () . e in dom (F _V) ) by Th5;
e DJoins () . e,() . e,G1 by ;
then (F _E) . e DJoins (F _V) . (() . e),(F _V) . (() . e),G2 by A1, A2, A3;
hence ( (the_Source_of G2) . ((F _E) . e) = (F _V) . (() . e) & () . ((F _E) . e) = (F _V) . (() . e) ) by GLIB_000:def 14; :: thesis: verum
end;
assume A4: for e being object st e in dom (F _E) holds
( () . ((F _E) . e) = (F _V) . (() . e) & () . ((F _E) . e) = (F _V) . (() . 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 & () . e = w ) by GLIB_000:def 14;
( (the_Source_of G2) . ((F _E) . e) = (F _V) . v & () . ((F _E) . e) = (F _V) . w ) by A4, A5, A6;
hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by ; :: thesis: verum