let A be set ; :: thesis: for f being Function st A c= bool (dom f) holds
f .: (union A) = union ((.: f) .: A)
let f be Function; :: thesis: ( A c= bool (dom f) implies f .: (union A) = union ((.: f) .: A) )
assume A1: A c= bool (dom f) ; :: thesis: f .: (union A) = union ((.: f) .: A)
A2: union ((.: f) .: A) c= f .: (union A) by Th15;
f .: (union A) c= union ((.: f) .: A)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (union A) or y in union ((.: f) .: A) )
assume y in f .: (union A) ; :: thesis: y in union ((.: f) .: A)
then consider x being set such that
x in dom f and
A3: x in union A and
A4: y = f . x by FUNCT_1:def 12;
consider X being set such that
A5: x in X and
A6: X in A by A3, TARSKI:def 4;
X in bool (dom f) by A1, A6;
then ( X in dom (.: f) & y in f .: X & (.: f) . X = f .: X ) by A4, A5, Def1, FUNCT_1:def 12;
then ( y in (.: f) . X & (.: f) . X in (.: f) .: A ) by A6, FUNCT_1:def 12;
hence y in union ((.: f) .: A) by TARSKI:def 4; :: thesis: verum

end;

hence f .: (union A) = union ((.: f) .: A) by A2, XBOOLE_0:def 10; :: thesis: verum