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

proof

let x be object ; :: thesis: ( x in X implies ((LMULT (X,R)) . ((1. R),f)) . x = f . x )
assume A0: x in X ; :: thesis: ((LMULT (X,R)) . ((1. R),f)) . x = f . x
then reconsider fx = f . x as Element of R by FUNCT_2:5;
((LMULT (X,R)) . ((1. R),f)) . x = (1. R) * fx by A0, Th2
.= f . x ;
hence ((LMULT (X,R)) . ((1. R),f)) . x = f . x ; :: thesis: verum

end;

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