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

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