let G1, G2, G3 be _Graph; :: thesis: for f being PVertexMapping of G1,G2
for g being PVertexMapping of G2,G3 st f is Disomorphism & g is Disomorphism holds
g * f is Disomorphism
let f be PVertexMapping of G1,G2; :: thesis: for g being PVertexMapping of G2,G3 st f is Disomorphism & g is Disomorphism holds
g * f is Disomorphism
let g be PVertexMapping of G2,G3; :: thesis: ( f is Disomorphism & g is Disomorphism implies g * f is Disomorphism )
assume A1: ( f is Disomorphism & g is Disomorphism ) ; :: thesis: g * f is Disomorphism
hence ( g * f is total & g * f is one-to-one & g * f is onto ) by FUNCT_2:27; :: according to GLIB_011:def 6 :: thesis: for v, w being Vertex of G1 holds
( card (G1 .edgesDBetween ({v},{w})) = card (G3 .edgesDBetween ({((g * f) . v)},{((g * f) . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G3 .edgesDBetween ({((g * f) . w)},{((g * f) . v)})) )
let v, w be Vertex of G1; :: thesis: ( card (G1 .edgesDBetween ({v},{w})) = card (G3 .edgesDBetween ({((g * f) . v)},{((g * f) . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G3 .edgesDBetween ({((g * f) . w)},{((g * f) . v)})) )
( v in the_Vertices_of G1 & w in the_Vertices_of G1 ) ;
then A2: ( v in dom f & w in dom f ) by A1, PARTFUN1:def 2;
then A3: ( f . v in rng f & f . w in rng f ) by FUNCT_1:3;
thus card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) by A1
.= card (G3 .edgesDBetween ({(g . (f . v))},{(g . (f . w))})) by A1, A3
.= card (G3 .edgesDBetween ({((g * f) . v)},{(g . (f . w))})) by A2, FUNCT_1:13
.= card (G3 .edgesDBetween ({((g * f) . v)},{((g * f) . w)})) by A2, FUNCT_1:13 ; :: thesis: card (G1 .edgesDBetween ({w},{v})) = card (G3 .edgesDBetween ({((g * f) . w)},{((g * f) . v)}))
thus card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) by A1
.= card (G3 .edgesDBetween ({(g . (f . w))},{(g . (f . v))})) by A1, A3
.= card (G3 .edgesDBetween ({((g * f) . w)},{(g . (f . v))})) by A2, FUNCT_1:13
.= card (G3 .edgesDBetween ({((g * f) . w)},{((g * f) . v)})) by A2, FUNCT_1:13 ; :: thesis: verum