now :: thesis: for a, b being Element of R holds (g * f) . (a * b) = ((g * f) . a) * ((g * f) . b)

let a, b be Element of R; :: thesis: (g * f) . (a * b) = ((g * f) . a) * ((g * f) . b)
A: dom f = the carrier of R by FUNCT_2:def 1;
hence (g * f) . (a * b) = g . (f . (a * b)) by FUNCT_1:13
.= g . ((f . a) * (f . b)) by GROUP_6:def 6
.= (g . (f . a)) * (g . (f . b)) by GROUP_6:def 6
.= ((g * f) . a) * (g . (f . b)) by A, FUNCT_1:13
.= ((g * f) . a) * ((g * f) . b) by A, FUNCT_1:13 ;
:: thesis: verum

end;

hence for b₁ being Function of R,T st b₁ = g * f holds
b₁ is multiplicative ; :: thesis: verum