let M, N be AbGroup; :: 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 = (f . x) + (g . x) by Th1
.= ((ADD (M,N)) . (g,f)) . x by Th1 ;
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