reconsider i = id the carrier of G as Homomorphism of G,G by GROUP_6:38;
i is bijective ;
hence ex b₁ being Endomorphism of G st b₁ is bijective ; :: thesis: verum