let R be Ring; :: thesis: for X being set
for f, g being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,g) = (ADD (X,R)) . (g,f)
let X be set ; :: thesis: for f, g being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,g) = (ADD (X,R)) . (g,f)
let f, g be Element of Funcs (X, the carrier of R); :: thesis: (ADD (X,R)) . (f,g) = (ADD (X,R)) . (g,f)
A0: ( dom ((ADD (X,R)) . (f,g)) = X & dom ((ADD (X,R)) . (g,f)) = X ) by FUNCT_2:92;
for x being object st x in X holds
((ADD (X,R)) . (f,g)) . x = ((ADD (X,R)) . (g,f)) . x

proof

let x be object ; :: thesis: ( x in X implies ((ADD (X,R)) . (f,g)) . x = ((ADD (X,R)) . (g,f)) . x )
assume A1: x in X ; :: thesis: ((ADD (X,R)) . (f,g)) . x = ((ADD (X,R)) . (g,f)) . x
then reconsider fx = f . x, gx = g . x as Element of R by FUNCT_2:5;
((ADD (X,R)) . (f,g)) . x = fx + gx by A1, Th1
.= gx + fx
.= ((ADD (X,R)) . (g,f)) . x by Th1, A1 ;
hence ((ADD (X,R)) . (f,g)) . x = ((ADD (X,R)) . (g,f)) . x ; :: thesis: verum

end;

hence (ADD (X,R)) . (f,g) = (ADD (X,R)) . (g,f) by A0; :: thesis: verum