let X, Y be 1-sorted ; :: thesis: for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds
f " ([#] Y) = [#] X
let f be Function of X,Y; :: thesis: ( ( [#] Y = {} implies [#] X = {} ) implies f " ([#] Y) = [#] X )
assume A1: ( [#] Y = {} implies [#] X = {} ) ; :: thesis: f " ([#] Y) = [#] X
f " (rng f) = dom f by RELAT_1:134
.= [#] X by A1, FUNCT_2:def 1 ;
then [#] X c= f " ([#] Y) by RELAT_1:143;
hence f " ([#] Y) = [#] X by XBOOLE_0:def 10; :: thesis: verum