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)

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

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (f " A) or x in f " (union A) )
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 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

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