let G be Group; :: thesis: ex h being Homomorphism of G,G st h is bijective
reconsider i = id the carrier of G as Homomorphism of G,G by Th38;
i is bijective ;
hence ex h being Homomorphism of G,G st h is bijective ; :: thesis: verum