let T be 1-sorted ; :: thesis: for S being non empty 1-sorted
for f being Function of T,S
for H being Subset-Family of S holds (" f) .: H is Subset-Family of T
let S be non empty 1-sorted ; :: thesis: for f being Function of T,S
for H being Subset-Family of S holds (" f) .: H is Subset-Family of T
let f be Function of T,S; :: thesis: for H being Subset-Family of S holds (" f) .: H is Subset-Family of T
let H be Subset-Family of S; :: thesis: (" f) .: H is Subset-Family of T
( (" f) .: H c= rng (" f) & rng (" f) c= bool (dom f) ) by FUNCT_3:22, RELAT_1:111;
then (" f) .: H c= bool (dom f) ;
hence (" f) .: H is Subset-Family of T by FUNCT_2:def 1; :: thesis: verum