let S, X be set ; :: thesis: for f being Function of S,X
for A being Subset of X st ( X = {} implies S = {} ) holds
(f " A) ` = f " (A ` )
let f be Function of S,X; :: thesis: for A being Subset of X st ( X = {} implies S = {} ) holds
(f " A) ` = f " (A ` )
let A be Subset of X; :: thesis: ( ( X = {} implies S = {} ) implies (f " A) ` = f " (A ` ) )
assume A1: ( X = {} implies S = {} ) ; :: thesis: (f " A) ` = f " (A ` )
A misses A ` by XBOOLE_1:79;
then A /\ (A ` ) = {} by XBOOLE_0:def 7;
then (f " A) /\ (f " (A ` )) = f " ({} X) by FUNCT_1:137
.= {} by RELAT_1:171 ;
then A2: f " A misses f " (A ` ) by XBOOLE_0:def 7;
(f " A) \/ (f " (A ` )) = f " (A \/ (A ` )) by RELAT_1:175
.= f " ([#] X) by SUBSET_1:25
.= [#] S by A1, Th48 ;
then ((f " A) ` ) /\ ((f " (A ` )) ` ) = ([#] S) ` by XBOOLE_1:53
.= {} S by XBOOLE_1:37 ;
then (f " A) ` misses (f " (A ` )) ` by XBOOLE_0:def 7;
hence (f " A) ` = f " (A ` ) by A2, SUBSET_1:46; :: thesis: verum