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:11;
hence ( dom T = [#] V & rng T c= [#] W ) by FUNCT_2:169; :: thesis: verum