let R be Ring; :: thesis: for M, N being LeftMod of R
for f being Element of Funcs ( the carrier of M, the carrier of N) holds (LMULT (M,N)) . [(1. R),f] = f
let M, N be LeftMod of R; :: thesis: for f being Element of Funcs ( the carrier of M, the carrier of N) holds (LMULT (M,N)) . [(1. R),f] = f
let f be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: (LMULT (M,N)) . [(1. R),f] = f
for x being Element of M holds ((LMULT (M,N)) . [(1. R),f]) . x = f . x

proof

let x be Element of M; :: thesis: ((LMULT (M,N)) . [(1. R),f]) . x = f . x
((LMULT (M,N)) . [(1. R),f]) . x = (1. R) * (f . x) by Th16
.= f . x ;
hence ((LMULT (M,N)) . [(1. R),f]) . x = f . x ; :: thesis: verum

end;

hence (LMULT (M,N)) . [(1. R),f] = f ; :: thesis: verum