let G1 be _Graph; :: thesis: for G2 being non-Dmulti _Graph
for F1, F2 being directed PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds
F1 = F2
let G2 be non-Dmulti _Graph; :: thesis: for F1, F2 being directed PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds
F1 = F2
let F1, F2 be directed PGraphMapping of G1,G2; :: thesis: ( F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) implies F1 = F2 )
assume that
A1: F1 _V = F2 _V and
A2: dom (F1 _E) = dom (F2 _E) ; :: thesis: F1 = F2
for e being object st e in dom (F1 _E) holds
(F1 _E) . e = (F2 _E) . e

proof

let e be object ; :: thesis: ( e in dom (F1 _E) implies (F1 _E) . e = (F2 _E) . e )
set v = (the_Source_of G1) . e;
set w = (the_Target_of G1) . e;
assume A3: e in dom (F1 _E) ; :: thesis: (F1 _E) . e = (F2 _E) . e
then A4: ( (the_Source_of G1) . e in dom (F1 _V) & (the_Target_of G1) . e in dom (F1 _V) ) by Th5;
A5: e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A3, GLIB_000:def 14;
then A6: (F1 _E) . e DJoins (F1 _V) . ((the_Source_of G1) . e),(F1 _V) . ((the_Target_of G1) . e),G2 by A3, A4, Def14;
A7: e in dom (F2 _E) by A2, A3;
then ( (the_Source_of G1) . e in dom (F2 _V) & (the_Target_of G1) . e in dom (F2 _V) ) by Th5;
then (F2 _E) . e DJoins (F1 _V) . ((the_Source_of G1) . e),(F2 _V) . ((the_Target_of G1) . e),G2 by A1, A5, A7, Def14;
hence (F1 _E) . e = (F2 _E) . e by A1, A6, GLIB_000:def 21; :: thesis: verum

end;

then F1 _E = F2 _E by A2, FUNCT_1:2;
hence F1 = F2 by A1, XTUPLE_0:2; :: thesis: verum