let T, S be non empty set ; :: thesis: for f being Function of T,S
for Q being Subset-Family of S holds union (f .: (f " Q)) c= union Q
let f be Function of T,S; :: thesis: for Q being Subset-Family of S holds union (f .: (f " Q)) c= union Q
let Q be Subset-Family of S; :: thesis: union (f .: (f " Q)) c= union Q
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (f .: (f " Q)) or x in union Q )
thus ( x in union (f .: (f " Q)) implies x in union Q ) :: thesis: verum

proof

assume x in union (f .: (f " Q)) ; :: thesis: x in union Q
then consider A being set such that
A1: ( x in A & A in f .: (f " Q) ) by TARSKI:def 4;
reconsider A = A as Subset of S by A1;
consider A1 being Subset of T such that
A2: ( A1 in f " Q & A = f .: A1 ) by A1, Def2a;
consider A2 being Subset of S such that
A3: ( A2 in Q & A1 = f " A2 ) by A2, Def10;
f .: (f " A2) c= A2 by FUNCT_1:145;
hence x in union Q by A1, A2, A3, TARSKI:def 4; :: thesis: verum

end;