let B be non empty set ; :: thesis: for f being Function holds f " (union B) = union { (f " Y) where Y is Element of B : verum }
let f be Function; :: thesis: f " (union B) = union { (f " Y) where Y is Element of B : verum }
set Z = { (f " Y) where Y is Element of B : verum } ;
thus f " (union B) c= union { (f " Y) where Y is Element of B : verum } :: according to XBOOLE_0:def 10 :: thesis: union { (f " Y) where Y is Element of B : verum } c= f " (union B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f " (union B) or x in union { (f " Y) where Y is Element of B : verum } )
assume A1: x in f " (union B) ; :: thesis: x in union { (f " Y) where Y is Element of B : verum }
then f . x in union B by FUNCT_1:def 7;
then consider Y being set such that
A2: f . x in Y and
A3: Y in B by TARSKI:def 4;
reconsider Y = Y as Element of B by A3;
x in dom f by A1, FUNCT_1:def 7;
then A4: x in f " Y by A2, FUNCT_1:def 7;
f " Y in { (f " Y) where Y is Element of B : verum } ;
hence x in union { (f " Y) where Y is Element of B : verum } by A4, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (f " Y) where Y is Element of B : verum } or x in f " (union B) )
assume x in union { (f " Y) where Y is Element of B : verum } ; :: thesis: x in f " (union B)
then consider Y being set such that
A5: x in Y and
A6: Y in { (f " Y) where Y is Element of B : verum } by TARSKI:def 4;
consider D being Element of B such that
A7: Y = f " D by A6;
f " D c= f " (union B) by RELAT_1:143, ZFMISC_1:74;
hence x in f " (union B) by A5, A7; :: thesis: verum