let V, W be non empty 1-sorted ; :: thesis: for T being Function of V,W holds
( dom T = [#] V & rng T c= [#] W )
let T be Function of V,W; :: thesis: ( dom T = [#] V & rng T c= [#] W )
T is Element of Funcs (([#] V),([#] W)) by FUNCT_2:8;
hence ( dom T = [#] V & rng T c= [#] W ) by FUNCT_2:92; :: thesis: verum