let G1, G2, G3 be _Graph; :: thesis: for f being PVertexMapping of G1,G2
for g being PVertexMapping of G2,G3 st f is isomorphism & g is isomorphism holds
g * f is isomorphism
let f be PVertexMapping of G1,G2; :: thesis: for g being PVertexMapping of G2,G3 st f is isomorphism & g is isomorphism holds
g * f is isomorphism
let g be PVertexMapping of G2,G3; :: thesis: ( f is isomorphism & g is isomorphism implies g * f is isomorphism )
assume A1: ( f is isomorphism & g is isomorphism ) ; :: thesis: g * f is isomorphism
hence ( g * f is total & g * f is one-to-one & g * f is onto ) by FUNCT_2:27; :: according to GLIB_011:def 5 :: thesis: for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G3 .edgesBetween ({((g * f) . v)},{((g * f) . w)}))
let v, w be Vertex of G1; :: thesis: card (G1 .edgesBetween ({v},{w})) = card (G3 .edgesBetween ({((g * f) . v)},{((g * f) . w)}))
( 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 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) by A1
.= card (G3 .edgesBetween ({(g . (f . v))},{(g . (f . w))})) by A1, A3
.= card (G3 .edgesBetween ({((g * f) . v)},{(g . (f . w))})) by A2, FUNCT_1:13
.= card (G3 .edgesBetween ({((g * f) . v)},{((g * f) . w)})) by A2, FUNCT_1:13 ; :: thesis: verum