let B be non empty set ; :: thesis: for f being Function holds f " () = union { (f " Y) where Y is Element of B : verum }
let f be Function; :: thesis: f " () = union { (f " Y) where Y is Element of B : verum }
set Z = { (f " Y) where Y is Element of B : verum } ;
thus f " () 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 " ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f " () or x in union { (f " Y) where Y is Element of B : verum } )
assume A1: x in f " () ; :: 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 ;
then A4: x in f " Y by ;
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 ; :: 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 " () )
assume x in union { (f " Y) where Y is Element of B : verum } ; :: thesis: x in f " ()
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 " () by ;
hence x in f " () by A5, A7; :: thesis: verum