let G be _Graph; :: thesis: id (the_Vertices_of G) is directed continuous Dcontinuous PVertexMapping of G,G
set f = id (the_Vertices_of G);

A1: now :: thesis: for v, w, e being object st v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e Joins v,w,G holds
ex e being object st e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G

let v, w, e be object ; :: thesis: ( v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e Joins v,w,G implies ex e being object st e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G )
assume A2: ( v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e Joins v,w,G ) ; :: thesis: ex e being object st e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G
take e = e; :: thesis: e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G
e Joins v,(id (the_Vertices_of G)) . w,G by A2, FUNCT_1:18;
hence e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G by A2, FUNCT_1:18; :: thesis: verum

end;

A3: now :: thesis: for v, w, e being object st v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e DJoins v,w,G holds
ex e being object st e DJoins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G

let v, w, e be object ; :: thesis: ( v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e DJoins v,w,G implies ex e being object st e DJoins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G )
assume A4: ( v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e DJoins v,w,G ) ; :: thesis: ex e being object st e DJoins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G
take e = e; :: thesis: e DJoins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G
e DJoins v,(id (the_Vertices_of G)) . w,G by A4, FUNCT_1:18;
hence e DJoins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G by A4, FUNCT_1:18; :: thesis: verum

end;

A5: now :: thesis: for v, w, e being object st v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G holds
ex e being object st e Joins v,w,G

let v, w, e be object ; :: thesis: ( v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G implies ex e being object st e Joins v,w,G )
assume A6: ( v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e Joins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G ) ; :: thesis: ex e being object st e Joins v,w,G
take e = e; :: thesis: e Joins v,w,G
e Joins v,(id (the_Vertices_of G)) . w,G by A6, FUNCT_1:18;
hence e Joins v,w,G by A6, FUNCT_1:18; :: thesis: verum

end;

now :: thesis: for v, w, e being object st v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e DJoins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G holds
ex e being object st e DJoins v,w,G

let v, w, e be object ; :: thesis: ( v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e DJoins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G implies ex e being object st e DJoins v,w,G )
assume A7: ( v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) & e DJoins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w,G ) ; :: thesis: ex e being object st e DJoins v,w,G
take e = e; :: thesis: e DJoins v,w,G
e DJoins v,(id (the_Vertices_of G)) . w,G by A7, FUNCT_1:18;
hence e DJoins v,w,G by A7, FUNCT_1:18; :: thesis: verum

end;

hence id (the_Vertices_of G) is directed continuous Dcontinuous PVertexMapping of G,G by A1, A3, A5, Th1, Th2, Def2, Def4; :: thesis: verum