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 A) = union (f " A)
let A be Subset-Family of Y; :: thesis: for f being Function of X,Y holds f " (union A) = union (f " A)
let f be Function of X,Y; :: thesis: f " (union A) = union (f " A)
thus f " (union A) c= union (f " A) :: according to XBOOLE_0:def 10 :: thesis: union (f " A) c= f " (union A)
proof
reconsider uA = union A as Subset of Y ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f " (union A) or x in union (f " A) )
assume A1: x in f " (union A) ; :: 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 A3, FUNCT_2:def 9;
x in f " YY by A1, A2, FUNCT_2:38;
hence x in union (f " A) by A4, TARSKI:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (f " A) or x in f " (union A) )
assume x in union (f " A) ; :: thesis: x in f " (union A)
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 A6, FUNCT_2:def 9;
f . x in B by A5, A9, FUNCT_1:def 7;
then f . x in union A by A8, TARSKI:def 4;
hence x in f " (union A) by A7, FUNCT_1:def 7; :: thesis: verum