per
cases
not ( the
carrier
of
T
=
{}
& not the
carrier
of
S
=
{}
& not ( the
carrier
of
T
=
{}
& the
carrier
of
S
<>
{}
) )
;
suppose
( the
carrier
of
T
=
{}
implies the
carrier
of
S
=
{}
) ;
:: thesis:
f

the
carrier
of
R
is
Function
of
R
,
T
hence
f

the
carrier
of
R
is
Function
of
R
,
T
by
A1
,
FUNCT_2:32
;
:: thesis:
verum
end;
suppose
A2
: ( the
carrier
of
T
=
{}
& the
carrier
of
S
<>
{}
) ;
:: thesis:
f

the
carrier
of
R
is
Function
of
R
,
T
then
f

the
carrier
of
R
=
{}
;
hence
f

the
carrier
of
R
is
Function
of
R
,
T
by
A2
,
Lm1
;
:: thesis:
verum
end;
end;