let
X
,
a
,
b
be
set
;
:: thesis:
for
f
being
Function
of
X
,
{
a
,
b
}
holds
X
=
(
f
"
{
a
}
)
\/
(
f
"
{
b
}
)
let
f
be
Function
of
X
,
{
a
,
b
}
;
:: thesis:
X
=
(
f
"
{
a
}
)
\/
(
f
"
{
b
}
)
thus
X
=
f
"
{
a
,
b
}
by
FUNCT_2:40
.=
f
"
(
{
a
}
\/
{
b
}
)
by
ENUMSET1:1
.=
(
f
"
{
a
}
)
\/
(
f
"
{
b
}
)
by
RELAT_1:140
;
:: thesis:
verum