set h = <-> f;
A1:
dom (<-> f) = dom f
by Def33;
rng (<-> f) c= I_PFuncs (DOMS Y)
proof
let y be
object ;
TARSKI:def 3 ( not y in rng (<-> f) or y in I_PFuncs (DOMS Y) )
assume
y in rng (<-> f)
;
y in I_PFuncs (DOMS Y)
then consider x being
object such that A2:
x in dom (<-> f)
and A3:
(<-> f) . x = y
by FUNCT_1:def 3;
reconsider y =
y as
Function by A3;
A4:
(<-> f) . x = - (f . x)
by A2, Def33;
A5:
rng y c= INT
by A3, A4, INT_1:def 2;
f . x in Y
by A1, A2, PARTFUN1:4;
then
dom (f . x) in { (dom m) where m is Element of Y : verum }
;
then A6:
dom (f . x) c= DOMS Y
by ZFMISC_1:74;
dom y = dom (f . x)
by A3, A4, VALUED_1:8;
then
y is
PartFunc of
(DOMS Y),
INT
by A6, A5, RELSET_1:4;
hence
y in I_PFuncs (DOMS Y)
by Def16;
verum
end;
hence
<-> f is PartFunc of X,(I_PFuncs (DOMS Y))
by A1, RELSET_1:4; verum