let G, H be Group; :: thesis: ( G,H are_isomorphic implies H,G are_isomorphic )
assume G,H are_isomorphic ; :: thesis: H,G are_isomorphic
then consider h being Homomorphism of G,H such that
A1: h is bijective ;
reconsider g = h " as Homomorphism of H,G by A1, Th62;
take g ; :: according to GROUP_6:def 11 :: thesis: g is bijective
thus g is bijective by A1, Th63; :: thesis: verum