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

for F being PGraphMapping of G1,G2 st F _V is one-to-one holds

F _E is one-to-one

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

F _E is one-to-one

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

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

for F being PGraphMapping of G1,G2 st F _V is one-to-one holds

F _E is one-to-one

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

F _E is one-to-one

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

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

now :: thesis: for e1, e2 being object st e1 in dom (F _E) & e2 in dom (F _E) & (F _E) . e1 = (F _E) . e2 holds

e1 = e2

hence
F _E is one-to-one
by FUNCT_1:def 4; :: thesis: verume1 = e2

let e1, e2 be object ; :: thesis: ( e1 in dom (F _E) & e2 in dom (F _E) & (F _E) . e1 = (F _E) . e2 implies b_{1} = b_{2} )

set v1 = (the_Source_of G1) . e1;

set w1 = (the_Target_of G1) . e1;

set v2 = (the_Source_of G1) . e2;

set w2 = (the_Target_of G1) . e2;

assume A2: ( e1 in dom (F _E) & e2 in dom (F _E) & (F _E) . e1 = (F _E) . e2 ) ; :: thesis: b_{1} = b_{2}

then A3: ( (the_Source_of G1) . e1 in dom (F _V) & (the_Target_of G1) . e1 in dom (F _V) & (the_Source_of G1) . e2 in dom (F _V) & (the_Target_of G1) . e2 in dom (F _V) ) by Th5;

A4: ( e1 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G1 & e2 Joins (the_Source_of G1) . e2,(the_Target_of G1) . e2,G1 ) by A2, GLIB_000:def 13;

then ( (F _E) . e1 Joins (F _V) . ((the_Source_of G1) . e1),(F _V) . ((the_Target_of G1) . e1),G2 & (F _E) . e2 Joins (F _V) . ((the_Source_of G1) . e2),(F _V) . ((the_Target_of G1) . e2),G2 ) by A2, A3, Th4;

end;set v1 = (the_Source_of G1) . e1;

set w1 = (the_Target_of G1) . e1;

set v2 = (the_Source_of G1) . e2;

set w2 = (the_Target_of G1) . e2;

assume A2: ( e1 in dom (F _E) & e2 in dom (F _E) & (F _E) . e1 = (F _E) . e2 ) ; :: thesis: b

then A3: ( (the_Source_of G1) . e1 in dom (F _V) & (the_Target_of G1) . e1 in dom (F _V) & (the_Source_of G1) . e2 in dom (F _V) & (the_Target_of G1) . e2 in dom (F _V) ) by Th5;

A4: ( e1 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G1 & e2 Joins (the_Source_of G1) . e2,(the_Target_of G1) . e2,G1 ) by A2, GLIB_000:def 13;

then ( (F _E) . e1 Joins (F _V) . ((the_Source_of G1) . e1),(F _V) . ((the_Target_of G1) . e1),G2 & (F _E) . e2 Joins (F _V) . ((the_Source_of G1) . e2),(F _V) . ((the_Target_of G1) . e2),G2 ) by A2, A3, Th4;

per cases then
( ( (F _V) . ((the_Source_of G1) . e1) = (F _V) . ((the_Source_of G1) . e2) & (F _V) . ((the_Target_of G1) . e1) = (F _V) . ((the_Target_of G1) . e2) ) or ( (F _V) . ((the_Source_of G1) . e1) = (F _V) . ((the_Target_of G1) . e2) & (F _V) . ((the_Target_of G1) . e1) = (F _V) . ((the_Source_of G1) . e2) ) )
by A2, GLIB_000:15;

end;

suppose
( (F _V) . ((the_Source_of G1) . e1) = (F _V) . ((the_Source_of G1) . e2) & (F _V) . ((the_Target_of G1) . e1) = (F _V) . ((the_Target_of G1) . e2) )
; :: thesis: b_{1} = b_{2}

then
( (the_Source_of G1) . e1 = (the_Source_of G1) . e2 & (the_Target_of G1) . e1 = (the_Target_of G1) . e2 )
by A1, A3, FUNCT_1:def 4;

hence e1 = e2 by A4, GLIB_000:def 20; :: thesis: verum

end;hence e1 = e2 by A4, GLIB_000:def 20; :: thesis: verum

suppose
( (F _V) . ((the_Source_of G1) . e1) = (F _V) . ((the_Target_of G1) . e2) & (F _V) . ((the_Target_of G1) . e1) = (F _V) . ((the_Source_of G1) . e2) )
; :: thesis: b_{1} = b_{2}

then
( (the_Source_of G1) . e1 = (the_Target_of G1) . e2 & (the_Target_of G1) . e1 = (the_Source_of G1) . e2 )
by A1, A3, FUNCT_1:def 4;

then e2 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G1 by A4, GLIB_000:14;

hence e1 = e2 by A4, GLIB_000:def 20; :: thesis: verum

end;then e2 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G1 by A4, GLIB_000:14;

hence e1 = e2 by A4, GLIB_000:def 20; :: thesis: verum