let A, X be set ; :: thesis: for D being non empty set
for f being Function of X,D st A c= bool X holds
f .: (union A) = union ((.: f) .: A)
let D be non empty set ; :: thesis: for f being Function of X,D st A c= bool X holds
f .: (union A) = union ((.: f) .: A)
let f be Function of X,D; :: thesis: ( A c= bool X implies f .: (union A) = union ((.: f) .: A) )
dom f = X by FUNCT_2:def 1;
hence ( A c= bool X implies f .: (union A) = union ((.: f) .: A) ) by Th14; :: thesis: verum