let S, T be 1-sorted ; :: thesis: for f being Function of S,T st T is empty & dom f = [#] S holds
S is empty
let f be Function of S,T; :: thesis: ( T is empty & dom f = [#] S implies S is empty )
assume that
A1: T is empty and
A2: dom f = [#] S ; :: thesis: S is empty
assume not S is empty ; :: thesis: contradiction
then reconsider S = S as non empty 1-sorted ;
consider x being object such that
A3: x in the carrier of S by XBOOLE_0:def 1;
f . x in rng f by A2, A3, FUNCT_1:def 3;
hence contradiction by A1; :: thesis: verum