let B be set ; :: thesis: for f being Function st B c= bool (rng f) holds
f " (union B) = union ((.: f) " B)
let f be Function; :: thesis: ( B c= bool (rng f) implies f " (union B) = union ((.: f) " B) )
assume A1: B c= bool (rng f) ; :: thesis: f " (union B) = union ((.: f) " B)
A2: f " (union B) c= union ((.: f) " B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f " (union B) or x in union ((.: f) " B) )
assume A3: x in f " (union B) ; :: thesis: x in union ((.: f) " B)
then f . x in union B by FUNCT_1:def 7;
then consider Y being set such that
A4: f . x in Y and
A5: Y in B by TARSKI:def 4;
A6: f " Y c= dom f by RELAT_1:132;
then f " Y in bool (dom f) ;
then A7: f " Y in dom (.: f) by Def1;
f .: (f " Y) = Y by A1, A5, FUNCT_1:77;
then (.: f) . (f " Y) in B by A5, A6, Def1;
then A8: f " Y in (.: f) " B by A7, FUNCT_1:def 7;
x in dom f by A3, FUNCT_1:def 7;
then x in f " Y by A4, FUNCT_1:def 7;
hence x in union ((.: f) " B) by A8, TARSKI:def 4; :: thesis: verum

end;

union ((.: f) " B) c= f " (union B) by Th16;
hence f " (union B) = union ((.: f) " B) by A2, XBOOLE_0:def 10; :: thesis: verum