let G1 be _Graph; :: thesis: for G2 being non-multi _Graph

for F1, F2 being PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds

F1 = F2

let G2 be non-multi _Graph; :: thesis: for F1, F2 being PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds

F1 = F2

let F1, F2 be 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

hence F1 = F2 by A1, XTUPLE_0:2; :: thesis: verum

for F1, F2 being PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds

F1 = F2

let G2 be non-multi _Graph; :: thesis: for F1, F2 being PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds

F1 = F2

let F1, F2 be 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

then
F1 _E = F2 _E
by A2, FUNCT_1:2;
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 Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A3, GLIB_000:def 13;

then A6: (F1 _E) . e Joins (F1 _V) . ((the_Source_of G1) . e),(F1 _V) . ((the_Target_of G1) . e),G2 by A3, A4, Th4;

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 Joins (F1 _V) . ((the_Source_of G1) . e),(F2 _V) . ((the_Target_of G1) . e),G2 by A1, A5, A7, Th4;

hence (F1 _E) . e = (F2 _E) . e by A1, A6, GLIB_000:def 20; :: thesis: verum

end;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 Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A3, GLIB_000:def 13;

then A6: (F1 _E) . e Joins (F1 _V) . ((the_Source_of G1) . e),(F1 _V) . ((the_Target_of G1) . e),G2 by A3, A4, Th4;

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 Joins (F1 _V) . ((the_Source_of G1) . e),(F2 _V) . ((the_Target_of G1) . e),G2 by A1, A5, A7, Th4;

hence (F1 _E) . e = (F2 _E) . e by A1, A6, GLIB_000:def 20; :: thesis: verum

hence F1 = F2 by A1, XTUPLE_0:2; :: thesis: verum