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: verumproof
let x,
y be
Element of
G;
:: thesis: (ZeroMap G,H) . (x + y) = ((ZeroMap G,H) . x) + ((ZeroMap G,H) . y)
(
(ZeroMap G,H) . (x + y) = 0. H &
(ZeroMap G,H) . x = 0. H &
(ZeroMap G,H) . y = 0. H )
by FUNCOP_1:13;
hence
(ZeroMap G,H) . (x + y) = ((ZeroMap G,H) . x) + ((ZeroMap G,H) . y)
by RLVECT_1:def 7;
:: thesis: verum
end;