now :: thesis: for x, y being Element of R holds (g * f) . (1. R) = 1. T
let x, y be Element of R; :: thesis: (g * f) . (1. R) = 1. T
dom f = the carrier of R by FUNCT_2:def 1;
hence (g * f) . (1. R) = g . (f . (1_ R)) by FUNCT_1:13
.= g . (1_ S) by GROUP_1:def 13
.= 1_ T by GROUP_1:def 13
.= 1. T ;
:: thesis: verum
end;
hence for b1 being Function of R,T st b1 = g * f holds
b1 is unity-preserving ; :: thesis: verum