let f be Function; :: thesis: ( f is empty implies f is constant )
assume A1: f is empty ; :: thesis: f is constant
let x be set ; :: according to FUNCT_1:def 10 :: 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 A1; :: thesis: verum