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 b₁ being Function of R,T st b₁ = g * f holds
b₁ is unity-preserving ; :: thesis: verum