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) = (LMULT (X,R)) . (a,((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) = (LMULT (X,R)) . (a,((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) = (LMULT (X,R)) . (a,((LMULT (X,R)) . (b,f)))
let f be Element of Funcs (X, the carrier of R); :: thesis: (LMULT (X,R)) . ((a * b),f) = (LMULT (X,R)) . (a,((LMULT (X,R)) . (b,f)))
set bf = (LMULT (X,R)) . (b,f);
B0: ( dom ((LMULT (X,R)) . ((a * b),f)) = X & dom ((LMULT (X,R)) . (a,((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 = ((LMULT (X,R)) . (a,((LMULT (X,R)) . (b,f)))) . x

proof

let x be object ; :: thesis: ( x in X implies ((LMULT (X,R)) . ((a * b),f)) . x = ((LMULT (X,R)) . (a,((LMULT (X,R)) . (b,f)))) . x )
assume A0: x in X ; :: thesis: ((LMULT (X,R)) . ((a * b),f)) . x = ((LMULT (X,R)) . (a,((LMULT (X,R)) . (b,f)))) . x
then reconsider fx = f . x as Element of R by FUNCT_2:5;
B1: 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 * (b * fx) by GROUP_1:def 3
.= ((LMULT (X,R)) . (a,((LMULT (X,R)) . (b,f)))) . x by B1, A0, Th2 ;
hence ((LMULT (X,R)) . ((a * b),f)) . x = ((LMULT (X,R)) . (a,((LMULT (X,R)) . (b,f)))) . x ; :: thesis: verum

end;

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