let f be Function; :: thesis: ( f is empty implies f is constant )
assume Z: f is empty ; :: thesis: f is constant
let x be set ; :: according to FUNCT_1:def 16 :: thesis: for y being set st x in dom f & y in dom f holds
f . x = f . y
thus for y being set st x in dom f & y in dom f holds
f . x = f . y by Z; :: thesis: verum