set f = id G;
rng (id G) = the carrier of G by RELAT_1:45;
then ( id G is one-to-one & id G is onto ) by FUNCT_2:def 3;
hence id G is bijective ; :: thesis: verum