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

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;

hence ZeroMap G,H is additive by Def13; :: thesis: verum