let c be Cardinal; :: thesis: for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism & G1 is c -regular holds
G2 is c -regular
let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism & G1 is c -regular holds
G2 is c -regular
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism & G1 is c -regular implies G2 is c -regular )
assume A1: ( F is isomorphism & G1 is c -regular ) ; :: thesis: G2 is c -regular
let v2 be Vertex of G2; :: according to GLIB_016:def 4 :: thesis: v2 .degree() = c
rng (F _V) = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v1 being object such that
A2: ( v1 in dom (F _V) & (F _V) . v1 = v2 ) by FUNCT_1:def 3;
reconsider v1 = v1 as Vertex of G1 by A2;
(F _V) /. v1 = (F _V) . v1 by A2, PARTFUN1:def 6;
hence v2 .degree() = v1 .degree() by A1, A2, GLIBPRE0:93
.= c by A1 ;
:: thesis: verum