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 = () . e;
set w = () . 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) & () . e in dom (F1 _V) ) by Th5;
A5: e DJoins () . e,() . e,G1 by ;
then A6: (F1 _E) . e DJoins (F1 _V) . (() . e),(F1 _V) . (() . e),G2 by ;
A7: e in dom (F2 _E) by A2, A3;
then ( (the_Source_of G1) . e in dom (F2 _V) & () . e in dom (F2 _V) ) by Th5;
then (F2 _E) . e DJoins (F1 _V) . (() . e),(F2 _V) . (() . e),G2 by A1, A5, A7, Def14;
hence (F1 _E) . e = (F2 _E) . e by ; :: thesis: verum
end;
then F1 _E = F2 _E by ;
hence F1 = F2 by ; :: thesis: verum