let G1, G2 be non-multi _Graph; :: thesis: for f being PVertexMapping of G1,G2 st f is continuous holds
PVM2PGM f is continuous
let f be PVertexMapping of G1,G2; :: thesis: ( f is continuous implies PVM2PGM f is continuous )
assume A1: f is continuous ; :: thesis: PVM2PGM f is continuous
now :: thesis: for e9, v, w being object st v in dom ((PVM2PGM f) _V) & w in dom ((PVM2PGM f) _V) & e9 Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 holds
ex e being object st
( e Joins v,w,G1 & e in dom ((PVM2PGM f) _E) & ((PVM2PGM f) _E) . e = e9 )
let e9, v, w be object ; :: thesis: ( v in dom ((PVM2PGM f) _V) & w in dom ((PVM2PGM f) _V) & e9 Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 implies ex e being object st
( e Joins v,w,G1 & e in dom ((PVM2PGM f) _E) & ((PVM2PGM f) _E) . e = e9 ) )
assume A2: ( v in dom ((PVM2PGM f) _V) & w in dom ((PVM2PGM f) _V) ) ; :: thesis: ( e9 Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 implies ex e being object st
( e Joins v,w,G1 & e in dom ((PVM2PGM f) _E) & ((PVM2PGM f) _E) . e = e9 ) )
assume A3: e9 Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 ; :: thesis: ex e being object st
( e Joins v,w,G1 & e in dom ((PVM2PGM f) _E) & ((PVM2PGM f) _E) . e = e9 )
then consider e being object such that
A4: e Joins v,w,G1 by A1, A2, Th2;
take e = e; :: thesis: ( e Joins v,w,G1 & e in dom ((PVM2PGM f) _E) & ((PVM2PGM f) _E) . e = e9 )
thus e Joins v,w,G1 by A4; :: thesis: ( e in dom ((PVM2PGM f) _E) & ((PVM2PGM f) _E) . e = e9 )
e in G1 .edgesBetween (dom ((PVM2PGM f) _V)) by A2, A4, GLIB_000:32;
hence e in dom ((PVM2PGM f) _E) by Def10; :: thesis: ((PVM2PGM f) _E) . e = e9
then ((PVM2PGM f) _E) . e Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 by A2, A4, GLIB_010:4;
hence ((PVM2PGM f) _E) . e = e9 by A3, GLIB_000:def 20; :: thesis: verum
end;
hence PVM2PGM f is continuous by GLIB_010:def 16; :: thesis: verum