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:38; :: 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 = {} by FUNCT_2:def 1;
then f | the carrier of R = {} ;
hence f | the carrier of R is Function of R,T by A2, FUNCTOR0:1; :: thesis: verum

end;

end;