let X, Y be non empty set ; :: thesis: for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( dom g = T .: (dom f) & dom g = (.: T) . (dom f) )
let T be Function of X,Y; :: thesis: for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( dom g = T .: (dom f) & dom g = (.: T) . (dom f) )
let f be PartFunc of X,ExtREAL; :: thesis: for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( dom g = T .: (dom f) & dom g = (.: T) . (dom f) )
let g be PartFunc of Y,ExtREAL; :: thesis: ( T is bijective & g = f * (T ") implies ( dom g = T .: (dom f) & dom g = (.: T) . (dom f) ) )
assume A1: ( T is bijective & g = f * (T ") ) ; :: thesis: ( dom g = T .: (dom f) & dom g = (.: T) . (dom f) )
then dom g = (T ") " (dom f) by RELAT_1:147;
hence dom g = T .: (dom f) by A1, FUNCT_1:84; :: thesis: dom g = (.: T) . (dom f)
hence dom g = (.: T) . (dom f) by A1, Th1; :: thesis: verum