let G1, G2 be non-multi _Graph; :: thesis: for f being PVertexMapping of G1,G2
for v being Vertex of G1 st f is isomorphism holds
v .degree() = (f /. v) .degree()
let f be PVertexMapping of G1,G2; :: thesis: for v being Vertex of G1 st f is isomorphism holds
v .degree() = (f /. v) .degree()
let v be Vertex of G1; :: thesis: ( f is isomorphism implies v .degree() = (f /. v) .degree() )
assume f is isomorphism ; :: thesis: v .degree() = (f /. v) .degree()
hence v .degree() = (((PVM2PGM f) _V) /. v) .degree() by Th99, GLIB_011:47
.= (f /. v) .degree() ;
:: thesis: verum