let R be Ring; :: thesis: for M, N being LeftMod of R
for x being Element of M
for f being Function of M,N holds x in dom f
let M, N be LeftMod of R; :: thesis: for x being Element of M
for f being Function of M,N holds x in dom f
let x be Element of M; :: thesis: for f being Function of M,N holds x in dom f
let f be Function of M,N; :: thesis: x in dom f
x in the carrier of M ;
hence x in dom f by FUNCT_2:def 1; :: thesis: verum