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)

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

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 union { (f " Y) where Y is Element of B : verum } or x in f " (union B) )
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;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

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