set f = R --> (0. S);
let x, y be Element of R; :: according to GROUP_6:def 6 :: thesis: (R --> (0. S)) . (x * y) = ((R --> (0. S)) . x) * ((R --> (0. S)) . y)
thus ((R --> (0. S)) . x) * ((R --> (0. S)) . y) = ((R --> (0. S)) . x) * (0. S) by FUNCOP_1:7
.= (R --> (0. S)) . (x * y) by FUNCOP_1:7 ; :: thesis: verum