let R be Ring; :: thesis: for M, N being LeftMod of R holds Func_Mod (R,M,N) is right_complementable
let M, N be LeftMod of R; :: thesis: Func_Mod (R,M,N) is right_complementable
let f be Element of (Func_Mod (R,M,N)); :: according to ALGSTR_0:def 16 :: thesis: f is right_complementable
reconsider g = (LMULT (M,N)) . [(- (1. R)),f] as Element of (Func_Mod (R,M,N)) by FUNCT_2:5;
take g ; :: according to ALGSTR_0:def 11 :: thesis: f + g = 0. (Func_Mod (R,M,N))
thus f + g = 0. (Func_Mod (R,M,N)) by Lm19; :: thesis: verum