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

proof

let x be Element of M; :: thesis: ((ADD (M,N)) . (f,g)) . x = ((ADD (M,N)) . (g,f)) . x
((ADD (M,N)) . (f,g)) . x = (g . x) + (f . x) by Th15
.= ((ADD (M,N)) . (g,f)) . x by Th15 ;
hence ((ADD (M,N)) . (f,g)) . x = ((ADD (M,N)) . (g,f)) . x ; :: thesis: verum

end;

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