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

proof

let x be object ; :: thesis: ( x in X implies ((LMULT (X,R)) . ((a + b),f)) . x = ((ADD (X,R)) . (((LMULT (X,R)) . (a,f)),((LMULT (X,R)) . (b,f)))) . x )
assume A0: x in X ; :: thesis: ((LMULT (X,R)) . ((a + b),f)) . x = ((ADD (X,R)) . (((LMULT (X,R)) . (a,f)),((LMULT (X,R)) . (b,f)))) . x
then reconsider fx = f . x as Element of R by FUNCT_2:5;
B1: a * fx = ((LMULT (X,R)) . (a,f)) . x by A0, Th2;
B2: b * fx = ((LMULT (X,R)) . (b,f)) . x by A0, Th2;
((LMULT (X,R)) . ((a + b),f)) . x = (a + b) * fx by A0, Th2
.= (a * fx) + (b * fx) by VECTSP_1:def 7
.= ((ADD (X,R)) . (((LMULT (X,R)) . (a,f)),((LMULT (X,R)) . (b,f)))) . x by A0, Th1, B1, B2 ;
hence ((LMULT (X,R)) . ((a + b),f)) . x = ((ADD (X,R)) . (((LMULT (X,R)) . (a,f)),((LMULT (X,R)) . (b,f)))) . x ; :: thesis: verum

end;

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