let R be Ring; :: thesis: for X being set
for f, g, h being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,((ADD (X,R)) . (g,h))) = (ADD (X,R)) . (((ADD (X,R)) . (f,g)),h)
let X be set ; :: thesis: for f, g, h being Element of Funcs (X, the carrier of R) holds (ADD (X,R)) . (f,((ADD (X,R)) . (g,h))) = (ADD (X,R)) . (((ADD (X,R)) . (f,g)),h)
let f, g, h be Element of Funcs (X, the carrier of R); :: thesis: (ADD (X,R)) . (f,((ADD (X,R)) . (g,h))) = (ADD (X,R)) . (((ADD (X,R)) . (f,g)),h)
set R1 = the carrier of R;
reconsider fg = (ADD (X,R)) . (f,g), gh = (ADD (X,R)) . (g,h) as Element of Funcs (X, the carrier of R) ;
set F1 = (ADD (X,R)) . (f,gh);
set F2 = (ADD (X,R)) . (fg,h);
B0: ( dom ((ADD (X,R)) . (f,gh)) = X & dom ((ADD (X,R)) . (fg,h)) = X ) by FUNCT_2:92;
for x being object st x in X holds
((ADD (X,R)) . (f,gh)) . x = ((ADD (X,R)) . (fg,h)) . x

proof

let x be object ; :: thesis: ( x in X implies ((ADD (X,R)) . (f,gh)) . x = ((ADD (X,R)) . (fg,h)) . x )
assume A1: x in X ; :: thesis: ((ADD (X,R)) . (f,gh)) . x = ((ADD (X,R)) . (fg,h)) . x
then reconsider fx = f . x, gx = g . x, hx = h . x as Element of R by FUNCT_2:5;
((ADD (X,R)) . (f,gh)) . x = the addF of R . (fx,(gh . x)) by A1, Th1
.= fx + (gx + hx) by A1, Th1
.= (fx + gx) + hx by RLVECT_1:def 3
.= the addF of R . ((fg . x),hx) by A1, Th1
.= ((ADD (X,R)) . (fg,h)) . x by A1, Th1 ;
hence ((ADD (X,R)) . (f,gh)) . x = ((ADD (X,R)) . (fg,h)) . x ; :: thesis: verum

end;

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