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 object ; :: 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 and
A2: A in f .: (f " Q) by TARSKI:def 4;
reconsider A = A as Subset of S by A2;
consider A1 being Subset of T such that
A3: A1 in f " Q and
A4: A = f .: A1 by A2, Def10;
consider A2 being Subset of S such that
A5: ( A2 in Q & A1 = f " A2 ) by A3, Def9;
f .: (f " A2) c= A2 by FUNCT_1:75;
hence x in union Q by A1, A4, A5, TARSKI:def 4; :: thesis: verum
end;