let G, H be AddGroup; :: thesis: for x, y being Element of G holds (ZeroMap (G,H)) . (x + y) = ((ZeroMap (G,H)) . x) + ((ZeroMap (G,H)) . y)
set f = ZeroMap (G,H);
thus for x, y being Element of G holds (ZeroMap (G,H)) . (x + y) = ((ZeroMap (G,H)) . x) + ((ZeroMap (G,H)) . y) :: thesis: verum

proof

let x, y be Element of G; :: thesis: (ZeroMap (G,H)) . (x + y) = ((ZeroMap (G,H)) . x) + ((ZeroMap (G,H)) . y)
A1: (ZeroMap (G,H)) . y = 0. H by FUNCOP_1:13;
( (ZeroMap (G,H)) . (x + y) = 0. H & (ZeroMap (G,H)) . x = 0. H ) by FUNCOP_1:13;
hence (ZeroMap (G,H)) . (x + y) = ((ZeroMap (G,H)) . x) + ((ZeroMap (G,H)) . y) by A1, RLVECT_1:def 7; :: thesis: verum

end;