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

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