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 9 :: 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