let T be non empty set ; :: thesis: for R being real-membered set
for f being Function of T,R holds incl (f,0) = T --> 0
let R be real-membered set ; :: thesis: for f being Function of T,R holds incl (f,0) = T --> 0
let f be Function of T,R; :: thesis: incl (f,0) = T --> 0
reconsider z = 0 as Element of (TOP-REAL 0) ;
incl (f,0) = T --> z

proof

let x be Element of T; :: according to FUNCT_2:def 8 :: thesis: (incl (f,0)) . x = (T --> z) . x
thus (incl (f,0)) . x = (T --> z) . x ; :: thesis: verum

end;

hence incl (f,0) = T --> 0 ; :: thesis: verum