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;