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 /\ (A `) = {} by XBOOLE_0:def 7, XBOOLE_1:79;
then (f " A) /\ (f " (A `)) = f " ({} X) by FUNCT_1:68
.= {} ;
then A2: f " A misses f " (A `) ;
(f " A) \/ (f " (A `)) = f " (A \/ (A `)) by RELAT_1:140
.= f " ([#] X) by SUBSET_1:10
.= [#] S by A1, Th39 ;
then ((f " A) `) /\ ((f " (A `)) `) = ([#] S) ` by XBOOLE_1:53
.= {} S by XBOOLE_1:37 ;
then (f " A) ` misses (f " (A `)) ` ;
hence (f " A) ` = f " (A `) by A2, SUBSET_1:25; :: thesis: verum