let X, Y be set ; :: thesis: for f being Function of X,Y
for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being object holds
( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds
g = f "
let f be Function of X,Y; :: thesis: for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being object holds
( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) holds
g = f "
let g be Function of Y,X; :: thesis: ( X <> {} & Y <> {} & rng f = Y & f is one-to-one & ( for y, x being object holds
( y in Y & g . y = x iff ( x in X & f . x = y ) ) ) implies g = f " )
assume ( X <> {} & Y <> {} ) ; :: thesis: ( not rng f = Y or not f is one-to-one or ex y, x being object st
( ( y in Y & g . y = x implies ( x in X & f . x = y ) ) implies ( x in X & f . x = y & not ( y in Y & g . y = x ) ) ) or g = f " )
then ( dom f = X & dom g = Y ) by Def1;
hence ( not rng f = Y or not f is one-to-one or ex y, x being object st
( ( y in Y & g . y = x implies ( x in X & f . x = y ) ) implies ( x in X & f . x = y & not ( y in Y & g . y = x ) ) ) or g = f " ) by FUNCT_1:32; :: thesis: verum