set h = f * g;

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

let a, b be Element of R; :: thesis: (f * g) . (a + b) = ((f * g) . a) + ((f * g) . b)
thus (f * g) . (a + b) = f . (g . (a + b)) by FUNCT_2:15
.= f . ((g . a) + (g . b)) by VECTSP_1:def 20
.= (f . (g . a)) + (f . (g . b)) by VECTSP_1:def 20
.= ((f * g) . a) + (f . (g . b)) by FUNCT_2:15
.= ((f * g) . a) + ((f * g) . b) by FUNCT_2:15 ; :: thesis: verum

end;

then A: f * g is additive ;

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

let a, b be Element of R; :: thesis: (f * g) . (a * b) = ((f * g) . a) * ((f * g) . b)
thus (f * g) . (a * b) = f . (g . (a * b)) by FUNCT_2:15
.= f . ((g . a) * (g . b)) by GROUP_6:def 6
.= (f . (g . a)) * (f . (g . b)) by GROUP_6:def 6
.= ((f * g) . a) * (f . (g . b)) by FUNCT_2:15
.= ((f * g) . a) * ((f * g) . b) by FUNCT_2:15 ; :: thesis: verum

end;

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