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

proof

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

proof

reconsider Y = Y as Subset of S by A3;
consider Y1 being Subset of T such that
A4: Y1 in f " B and
A5: Y = f .: Y1 by A3, Def10;
consider Y2 being Subset of S such that
A6: ( Y2 in B & Y1 = f " Y2 ) by A4, Def9;
A7: f .: (f " Y2) c= Y2 by FUNCT_1:75;
reconsider Y2 = Y2 as set ;
take Y2 ; :: thesis: ( x in Y2 & Y2 in B )
thus ( x in Y2 & Y2 in B ) by A2, A5, A6, A7; :: thesis: verum

end;

hence x in union B by TARSKI:def 4; :: thesis: verum

end;

hence B is Cover of P by SETFAM_1:def 11; :: thesis: verum