let T, S be non empty set ; :: thesis: for f being Function of T,S
for P being Subset-Family of T holds union P c= union (f " (f .: P))
let f be Function of T,S; :: thesis: for P being Subset-Family of T holds union P c= union (f " (f .: P))
let P be Subset-Family of T; :: thesis: union P c= union (f " (f .: P))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union P or x in union (f " (f .: P)) )
assume x in union P ; :: thesis: x in union (f " (f .: P))
then consider A being set such that
A1: x in A and
A2: A in P by TARSKI:def 4;
A3: A c= T by A2;
reconsider A = A as Subset of T by A2;
reconsider A1 = f .: A as Subset of S ;
reconsider A2 = f " A1 as Subset of T ;
A c= dom f by A3, Def1;
then A4: A c= A2 by FUNCT_1:76;
A1 in f .: P by A2, Def10;
then A2 in f " (f .: P) by Def9;
hence x in union (f " (f .: P)) by A1, A4, TARSKI:def 4; :: thesis: verum