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