let G be non empty addLoopStr ; :: thesis: id G is additive
set f = id G;
for x, y being Element of G holds (id G) . (x + y) = ((id G) . x) + ((id G) . y)

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;

hence id G is additive by Def13; :: thesis: verum