let X be set ; :: thesis: for Y being non empty set
for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
let Y be non empty set ; :: thesis: for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
let f be Function of X,Y; :: thesis: for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
let H be Subset-Family of X; :: thesis: union ((.: f) .: H) = f .: (union H)
dom f = X by FUNCT_2:def 1;
hence union ((.: f) .: H) = f .: (union H) by FUNCT_3:14; :: thesis: verum