set f = id G;
let x, y be Element of G; :: according to VECTSP_1:def 19 :: thesis: (id G) . (x + y) = ((id G) . x) + ((id G) . y)
( (id G) . (x + y) = x + y & (id G) . x = x ) by FUNCT_1:18;
hence (id G) . (x + y) = ((id G) . x) + ((id G) . y) by FUNCT_1:18; :: thesis: verum