let G1, G2 be _Graph; :: thesis: for F being one-to-one PGraphMapping of G1,G2 st F is isomorphism holds

( F * (F ") = id G2 & (F ") * F = id G1 )

let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ( F * (F ") = id G2 & (F ") * F = id G1 ) )

assume A1: F is isomorphism ; :: thesis: ( F * (F ") = id G2 & (F ") * F = id G1 )

thus F * (F ") = [(id (rng (F _V))),((F _E) * ((F _E) "))] by FUNCT_1:39

.= [(id (rng (F _V))),(id (rng (F _E)))] by FUNCT_1:39

.= [(id (the_Vertices_of G2)),(id (rng (F _E)))] by A1, Def12

.= id G2 by A1, Def12 ; :: thesis: (F ") * F = id G1

thus (F ") * F = [(id (dom (F _V))),(((F _E) ") * (F _E))] by FUNCT_1:39

.= [(id (dom (F _V))),(id (dom (F _E)))] by FUNCT_1:39

.= [(id (the_Vertices_of G1)),(id (dom (F _E)))] by A1, Def11

.= id G1 by A1, Def11 ; :: thesis: verum

( F * (F ") = id G2 & (F ") * F = id G1 )

let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ( F * (F ") = id G2 & (F ") * F = id G1 ) )

assume A1: F is isomorphism ; :: thesis: ( F * (F ") = id G2 & (F ") * F = id G1 )

thus F * (F ") = [(id (rng (F _V))),((F _E) * ((F _E) "))] by FUNCT_1:39

.= [(id (rng (F _V))),(id (rng (F _E)))] by FUNCT_1:39

.= [(id (the_Vertices_of G2)),(id (rng (F _E)))] by A1, Def12

.= id G2 by A1, Def12 ; :: thesis: (F ") * F = id G1

thus (F ") * F = [(id (dom (F _V))),(((F _E) ") * (F _E))] by FUNCT_1:39

.= [(id (dom (F _V))),(id (dom (F _E)))] by FUNCT_1:39

.= [(id (the_Vertices_of G1)),(id (dom (F _E)))] by A1, Def11

.= id G1 by A1, Def11 ; :: thesis: verum