let
I
be
set
;
:: thesis:
uncurry
(
I
-->
{}
)
=
{}
per
cases
(
I
=
{}
or
I
<>
{}
)
;
suppose
I
=
{}
;
:: thesis:
uncurry
(
I
-->
{}
)
=
{}
hence
uncurry
(
I
-->
{}
)
=
{}
by
FUNCT_5:43
;
:: thesis:
verum
end;
suppose
I
<>
{}
;
:: thesis:
uncurry
(
I
-->
{}
)
=
{}
then
rng
(
I
-->
{}
)
=
{
{}
}
by
FUNCOP_1:8
.=
Funcs
(
{}
,
{}
)
by
FUNCT_5:57
;
then
dom
(
uncurry
(
I
-->
{}
)
)
=
[:
(
dom
(
I
-->
{}
)
)
,
{}
:]
by
FUNCT_5:26
.=
{}
by
ZFMISC_1:90
;
hence
uncurry
(
I
-->
{}
)
=
{}
;
:: thesis:
verum
end;
end;