let c be Cardinal; :: thesis: for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Disomorphism & G1 is c -Dregular holds
G2 is c -Dregular
let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is Disomorphism & G1 is c -Dregular holds
G2 is c -Dregular
let F be PGraphMapping of G1,G2; :: thesis: ( F is Disomorphism & G1 is c -Dregular implies G2 is c -Dregular )
assume A1: ( F is Disomorphism & G1 is c -Dregular ) ; :: thesis: G2 is c -Dregular
let v2 be Vertex of G2; :: according to GLIB_016:def 8 :: thesis: ( v2 .inDegree() = c & v2 .outDegree() = 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;
A3: (F _V) /. v1 = (F _V) . v1 by A2, PARTFUN1:def 6;
hence v2 .inDegree() = v1 .inDegree() by A1, A2, GLIBPRE0:92
.= c by A1 ;
:: thesis: v2 .outDegree() = c
thus v2 .outDegree() = v1 .outDegree() by A1, A2, A3, GLIBPRE0:92
.= c by A1 ; :: thesis: verum