let X, Y be non empty TopSpace; :: thesis: for A being Subset-Family of Y
for f being Function of X,Y holds f " () = union (f " A)

let A be Subset-Family of Y; :: thesis: for f being Function of X,Y holds f " () = union (f " A)
let f be Function of X,Y; :: thesis: f " () = union (f " A)
thus f " () c= union (f " A) :: according to XBOOLE_0:def 10 :: thesis: union (f " A) c= f " ()
proof
reconsider uA = union A as Subset of Y ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f " () or x in union (f " A) )
assume A1: x in f " () ; :: thesis: x in union (f " A)
then f . x in uA by FUNCT_2:38;
then consider YY being set such that
A2: f . x in YY and
A3: YY in A by TARSKI:def 4;
reconsider fY = f " YY as Subset of X ;
A4: fY in f " A by ;
x in f " YY by ;
hence x in union (f " A) by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (f " A) or x in f " () )
assume x in union (f " A) ; :: thesis: x in f " ()
then consider YY being set such that
A5: x in YY and
A6: YY in f " A by TARSKI:def 4;
x in the carrier of X by A5, A6;
then A7: x in dom f by FUNCT_2:def 1;
reconsider B1 = YY as Subset of X by A6;
consider B being Subset of Y such that
A8: B in A and
A9: B1 = f " B by ;
f . x in B by ;
then f . x in union A by ;
hence x in f " () by ; :: thesis: verum