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

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