reconsider f = Y --> FALSE as Function of Y,BOOLEAN ;
reconsider f = f as Function of Y,BOOLEAN ;
take f ; :: thesis: for x being Element of Y holds f . x = FALSE
let x be Element of Y; :: thesis: f . x = FALSE
thus f . x = FALSE ; :: thesis: verum