let G be AddGroup; :: thesis: ( ( for x, y being Element of G holds (id G) . (x + y) = ((id G) . x) + ((id G) . y) ) & id G is one-to-one & id G is onto )
set f = id G;
thus for x, y being Element of G holds (id G) . (x + y) = ((id G) . x) + ((id G) . y) :: thesis: ( id G is one-to-one & id G is onto )

proof

let x, y be Element of G; :: thesis: (id G) . (x + y) = ((id G) . x) + ((id G) . y)
( (id G) . (x + y) = x + y & (id G) . x = x & (id G) . y = y ) by FUNCT_1:35;
hence (id G) . (x + y) = ((id G) . x) + ((id G) . y) ; :: thesis: verum

end;

thus id G is one-to-one by FUNCT_1:52; :: thesis: id G is onto
thus rng (id G) = the carrier of G by RELAT_1:71; :: according to FUNCT_2:def 3 :: thesis: verum