let M be AbGroup; :: thesis: for f being Element of Funcs ( the carrier of M, the carrier of M) holds (ADD (M,M)) . (f,(ZeroMap (M,M))) = f
let f be Element of Funcs ( the carrier of M, the carrier of M); :: thesis: (ADD (M,M)) . (f,(ZeroMap (M,M))) = f
reconsider z = ZeroMap (M,M) as Element of Funcs ( the carrier of M, the carrier of M) by FUNCT_2:8;
for x being Element of M holds ((ADD (M,M)) . (f,z)) . x = f . x

proof

let x be Element of M; :: thesis: ((ADD (M,M)) . (f,z)) . x = f . x
((ADD (M,M)) . (f,z)) . x = (f . x) + (z . x) by Th1
.= (f . x) + (( the carrier of M --> (0. M)) . x) by GRCAT_1:def 7
.= (f . x) + (0. M) ;
hence ((ADD (M,M)) . (f,z)) . x = f . x by RLVECT_1:def 4; :: thesis: verum

end;

then (ADD (M,M)) . (f,z) = f ;
hence (ADD (M,M)) . (f,(ZeroMap (M,M))) = f ; :: thesis: verum