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