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