let S, T be 1-sorted ; :: thesis: for f being Function of S,T st S is empty & rng f = [#] T holds

T is empty

let f be Function of S,T; :: thesis: ( S is empty & rng f = [#] T implies T is empty )

assume that

A1: S is empty and

A2: rng f = [#] T ; :: thesis: T is empty

assume not T is empty ; :: thesis: contradiction

then reconsider T = T as non empty 1-sorted ;

consider y being object such that

A3: y in the carrier of T by XBOOLE_0:def 1;

ex x being object st

( x in dom f & f . x = y ) by A2, A3, FUNCT_1:def 3;

hence contradiction by A1; :: thesis: verum

T is empty

let f be Function of S,T; :: thesis: ( S is empty & rng f = [#] T implies T is empty )

assume that

A1: S is empty and

A2: rng f = [#] T ; :: thesis: T is empty

assume not T is empty ; :: thesis: contradiction

then reconsider T = T as non empty 1-sorted ;

consider y being object such that

A3: y in the carrier of T by XBOOLE_0:def 1;

ex x being object st

( x in dom f & f . x = y ) by A2, A3, FUNCT_1:def 3;

hence contradiction by A1; :: thesis: verum