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;