let
f
be
Function
of
[:
{
o
}
,
{
m
}
:]
,
{
r
}
;
:: thesis:
(
f
=
(
o
,
m
)
.-->
r
iff verum )
(
o
,
m
)
.-->
r
is
Function
of
[:
{
o
}
,
{
m
}
:]
,
{
r
}
by
Lm2
;
hence
(
f
=
(
o
,
m
)
.-->
r
iff verum )
by
FUNCT_2:51
;
:: thesis:
verum