let G1, G2 be _Graph; :: thesis: for F being Dcontinuous PGraphMapping of G1,G2 st F _E is one-to-one holds

F is directed

let F be Dcontinuous PGraphMapping of G1,G2; :: thesis: ( F _E is one-to-one implies F is directed )

assume A1: F _E is one-to-one ; :: thesis: F is directed

thus verum ; :: thesis: verum

F is directed

let F be Dcontinuous PGraphMapping of G1,G2; :: thesis: ( F _E is one-to-one implies F is directed )

assume A1: F _E is one-to-one ; :: thesis: F is directed

now :: thesis: for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 holds

(F _E) . e DJoins (F _V) . v,(F _V) . w,G2

hence
F is directed
; :: thesis: verum(F _E) . e DJoins (F _V) . v,(F _V) . w,G2

let e, v, w be object ; :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 implies (F _E) . b_{1} DJoins (F _V) . b_{2},(F _V) . b_{3},G2 )

assume A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( e DJoins v,w,G1 implies (F _E) . b_{1} DJoins (F _V) . b_{2},(F _V) . b_{3},G2 )

assume A3: e DJoins v,w,G1 ; :: thesis: (F _E) . b_{1} DJoins (F _V) . b_{2},(F _V) . b_{3},G2

then e Joins v,w,G1 by GLIB_000:16;

end;assume A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( e DJoins v,w,G1 implies (F _E) . b

assume A3: e DJoins v,w,G1 ; :: thesis: (F _E) . b

then e Joins v,w,G1 by GLIB_000:16;

per cases then
( (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 or (F _E) . e DJoins (F _V) . w,(F _V) . v,G2 )
by A2, Th4, GLIB_000:16;

end;

suppose
(F _E) . e DJoins (F _V) . v,(F _V) . w,G2
; :: thesis: (F _E) . b_{1} DJoins (F _V) . b_{2},(F _V) . b_{3},G2

end;

end;

suppose A4:
(F _E) . e DJoins (F _V) . w,(F _V) . v,G2
; :: thesis: (F _E) . b_{1} DJoins (F _V) . b_{2},(F _V) . b_{3},G2

then consider e0 being object such that

A5: ( e0 DJoins w,v,G1 & e0 in dom (F _E) & (F _E) . e0 = (F _E) . e ) by A2, Def18;

e0 = e by A1, A2, A5, FUNCT_1:def 4;

then v = w by A3, A5, GLIB_009:6;

hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A4; :: thesis: verum

end;A5: ( e0 DJoins w,v,G1 & e0 in dom (F _E) & (F _E) . e0 = (F _E) . e ) by A2, Def18;

e0 = e by A1, A2, A5, FUNCT_1:def 4;

then v = w by A3, A5, GLIB_009:6;

hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A4; :: thesis: verum

thus verum ; :: thesis: verum