let M, N be AbGroup; :: 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