let G1, G2 be non-Dmulti _Graph; :: thesis: for f being directed PVertexMapping of G1,G2 st f is Dcontinuous holds
DPVM2PGM f is Dcontinuous
let f be directed PVertexMapping of G1,G2; :: thesis: ( f is Dcontinuous implies DPVM2PGM f is Dcontinuous )
assume A1: f is Dcontinuous ; :: thesis: DPVM2PGM f is Dcontinuous
now :: thesis: for e9, v, w being object st v in dom ((DPVM2PGM f) _V) & w in dom ((DPVM2PGM f) _V) & e9 DJoins ((DPVM2PGM f) _V) . v,((DPVM2PGM f) _V) . w,G2 holds
ex e being object st
( e DJoins v,w,G1 & e in dom ((DPVM2PGM f) _E) & ((DPVM2PGM f) _E) . e = e9 )
let e9, v, w be object ; :: thesis: ( v in dom ((DPVM2PGM f) _V) & w in dom ((DPVM2PGM f) _V) & e9 DJoins ((DPVM2PGM f) _V) . v,((DPVM2PGM f) _V) . w,G2 implies ex e being object st
( e DJoins v,w,G1 & e in dom ((DPVM2PGM f) _E) & ((DPVM2PGM f) _E) . e = e9 ) )
assume A2: ( v in dom ((DPVM2PGM f) _V) & w in dom ((DPVM2PGM f) _V) ) ; :: thesis: ( e9 DJoins ((DPVM2PGM f) _V) . v,((DPVM2PGM f) _V) . w,G2 implies ex e being object st
( e DJoins v,w,G1 & e in dom ((DPVM2PGM f) _E) & ((DPVM2PGM f) _E) . e = e9 ) )
then reconsider v0 = v, w0 = w as Vertex of G1 ;
assume A3: e9 DJoins ((DPVM2PGM f) _V) . v,((DPVM2PGM f) _V) . w,G2 ; :: thesis: ex e being object st
( e DJoins v,w,G1 & e in dom ((DPVM2PGM f) _E) & ((DPVM2PGM f) _E) . e = e9 )
then consider e being object such that
A4: e DJoins v,w,G1 by A1, A2;
take e = e; :: thesis: ( e DJoins v,w,G1 & e in dom ((DPVM2PGM f) _E) & ((DPVM2PGM f) _E) . e = e9 )
thus e DJoins v,w,G1 by A4; :: thesis: ( e in dom ((DPVM2PGM f) _E) & ((DPVM2PGM f) _E) . e = e9 )
e Joins v,w,G1 by A4, GLIB_000:16;
then e in G1 .edgesBetween (dom ((DPVM2PGM f) _V)) by A2, GLIB_000:32;
hence e in dom ((DPVM2PGM f) _E) by Def11; :: thesis: ((DPVM2PGM f) _E) . e = e9
then ((DPVM2PGM f) _E) . e DJoins ((DPVM2PGM f) _V) . v,((DPVM2PGM f) _V) . w,G2 by A2, A4, GLIB_010:def 14;
hence ((DPVM2PGM f) _E) . e = e9 by A3, GLIB_000:def 21; :: thesis: verum
end;
hence DPVM2PGM f is Dcontinuous by GLIB_010:def 18; :: thesis: verum