let G1, G2 be non-Dmulti _Graph; :: thesis: for f being directed PVertexMapping of G1,G2
for v being Vertex of G1 st f is Disomorphism holds
( v .inDegree() = (f /. v) .inDegree() & v .outDegree() = (f /. v) .outDegree() )
let f be directed PVertexMapping of G1,G2; :: thesis: for v being Vertex of G1 st f is Disomorphism holds
( v .inDegree() = (f /. v) .inDegree() & v .outDegree() = (f /. v) .outDegree() )
let v be Vertex of G1; :: thesis: ( f is Disomorphism implies ( v .inDegree() = (f /. v) .inDegree() & v .outDegree() = (f /. v) .outDegree() ) )
assume f is Disomorphism ; :: thesis: ( v .inDegree() = (f /. v) .inDegree() & v .outDegree() = (f /. v) .outDegree() )
then A1: DPVM2PGM f is Disomorphism by GLIB_011:48;
thus v .inDegree() = (((DPVM2PGM f) _V) /. v) .inDegree() by A1, Th98
.= (f /. v) .inDegree() ; :: thesis: v .outDegree() = (f /. v) .outDegree()
thus v .outDegree() = (((DPVM2PGM f) _V) /. v) .outDegree() by A1, Th98
.= (f /. v) .outDegree() ; :: thesis: verum