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

proof

let x be object ; :: thesis: ( x in X implies ((ADD (X,R)) . (((LMULT (X,R)) . (a,f)),((LMULT (X,R)) . (a,g)))) . x = ((LMULT (X,R)) . (a,((ADD (X,R)) . (f,g)))) . x )
assume A0: x in X ; :: thesis: ((ADD (X,R)) . (((LMULT (X,R)) . (a,f)),((LMULT (X,R)) . (a,g)))) . x = ((LMULT (X,R)) . (a,((ADD (X,R)) . (f,g)))) . x
then reconsider fgx = ((ADD (X,R)) . (f,g)) . x as Element of R by FUNCT_2:5;
reconsider fx = f . x, gx = g . x as Element of R by A0, FUNCT_2:5;
A2: the addF of R . (( the multF of R . (a,(f . x))),( the multF of R . (a,(g . x)))) = (a * fx) + (a * gx)
.= a * (fx + gx) by VECTSP_1:def 7
.= a * fgx by A0, Th1 ;
A5: a * fx = ((LMULT (X,R)) . (a,f)) . x by A0, Th2;
a * gx = ((LMULT (X,R)) . (a,g)) . x by A0, Th2;
then ((ADD (X,R)) . (((LMULT (X,R)) . (a,f)),((LMULT (X,R)) . (a,g)))) . x = a * fgx by A2, A5, A0, Th1
.= ((LMULT (X,R)) . (a,((ADD (X,R)) . (f,g)))) . x by A0, Th2 ;
hence ((ADD (X,R)) . (((LMULT (X,R)) . (a,f)),((LMULT (X,R)) . (a,g)))) . x = ((LMULT (X,R)) . (a,((ADD (X,R)) . (f,g)))) . x ; :: thesis: verum

end;

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