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
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
let e1, e2 be object ; :: thesis: ( e1 in dom (F _E) & e2 in dom (F _E) & (F _E) . e1 = (F _E) . e2 implies b1 = b2 )
set v1 = () . e1;
set w1 = () . e1;
set v2 = () . e2;
set w2 = () . e2;
assume A2: ( e1 in dom (F _E) & e2 in dom (F _E) & (F _E) . e1 = (F _E) . e2 ) ; :: thesis: b1 = b2
then A3: ( (the_Source_of G1) . e1 in dom (F _V) & () . e1 in dom (F _V) & () . e2 in dom (F _V) & () . e2 in dom (F _V) ) by Th5;
A4: ( e1 Joins () . e1,() . e1,G1 & e2 Joins () . e2,() . e2,G1 ) by ;
then ( (F _E) . e1 Joins (F _V) . (() . e1),(F _V) . (() . e1),G2 & (F _E) . e2 Joins (F _V) . (() . e2),(F _V) . (() . e2),G2 ) by A2, A3, Th4;
per cases ) . (() . e1) = (F _V) . (() . e2) & (F _V) . (() . e1) = (F _V) . (() . e2) ) or ( (F _V) . (() . e1) = (F _V) . (() . e2) & (F _V) . (() . e1) = (F _V) . (() . e2) ) ) by ;
suppose ( (F _V) . (() . e1) = (F _V) . (() . e2) & (F _V) . (() . e1) = (F _V) . (() . e2) ) ; :: thesis: b1 = b2
then ( (the_Source_of G1) . e1 = () . e2 & () . e1 = () . e2 ) by ;
hence e1 = e2 by ; :: thesis: verum
end;
suppose ( (F _V) . (() . e1) = (F _V) . (() . e2) & (F _V) . (() . e1) = (F _V) . (() . e2) ) ; :: thesis: b1 = b2
then ( (the_Source_of G1) . e1 = () . e2 & () . e1 = () . e2 ) by ;
then e2 Joins () . e1,() . e1,G1 by ;
hence e1 = e2 by ; :: thesis: verum
end;
end;
end;
hence F _E is one-to-one by FUNCT_1:def 4; :: thesis: verum