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

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

hence
incl (f,0) = T --> 0
; :: thesis: verum
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;thus (incl (f,0)) . x = (T --> z) . x ; :: thesis: verum