let T, S be non empty set ; :: thesis: for f being Function of T,S
for B being Subset-Family of T
for P being Subset of T st B is Cover of P holds
f " (f .: B) is Cover of P
let f be Function of T,S; :: thesis: for B being Subset-Family of T
for P being Subset of T st B is Cover of P holds
f " (f .: B) is Cover of P
let B be Subset-Family of T; :: thesis: for P being Subset of T st B is Cover of P holds
f " (f .: B) is Cover of P
let P be Subset of T; :: thesis: ( B is Cover of P implies f " (f .: B) is Cover of P )
assume B is Cover of P ; :: thesis: f " (f .: B) is Cover of P
then A1: P c= union B by SETFAM_1:def 11;
P c= union (f " (f .: B))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in union (f " (f .: B)) )
assume x in P ; :: thesis: x in union (f " (f .: B))
then consider Y being set such that
A2: x in Y and
A3: Y in B by A1, TARSKI:def 4;
ex Z being set st
( x in Z & Z in f " (f .: B) )

proof

reconsider Y = Y as Subset of T by A3;
set Z = f " (f .: Y);
take f " (f .: Y) ; :: thesis: ( x in f " (f .: Y) & f " (f .: Y) in f " (f .: B) )
dom f = T by Def1;
then A4: Y c= f " (f .: Y) by FUNCT_1:76;
f .: Y in f .: B by A3, Def10;
hence ( x in f " (f .: Y) & f " (f .: Y) in f " (f .: B) ) by A2, A4, Def9; :: thesis: verum

end;

hence x in union (f " (f .: B)) by TARSKI:def 4; :: thesis: verum

end;

hence f " (f .: B) is Cover of P by SETFAM_1:def 11; :: thesis: verum