let R be Ring; :: thesis: for M, N being LeftMod of R
for f being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,(0_Funcs (M,N))) = f
let M, N be LeftMod of R; :: thesis: for f being Element of Funcs ( the carrier of M, the carrier of N) holds (ADD (M,N)) . (f,(0_Funcs (M,N))) = f
let f be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: (ADD (M,N)) . (f,(0_Funcs (M,N))) = f
set F1 = (ADD (M,N)) . (f,(0_Funcs (M,N)));
for x being Element of M holds ((ADD (M,N)) . (f,(0_Funcs (M,N)))) . x = f . x

proof

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

end;

hence (ADD (M,N)) . (f,(0_Funcs (M,N))) = f ; :: thesis: verum