reconsider f = Y --> FALSE as Function of Y,BOOLEAN ;
reconsider f = f as Element of Funcs (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 by FUNCOP_1:7; :: thesis: verum