consider H being non empty multMagma ;
set f = I --> H;
take I --> H ; :: thesis: I --> H is multMagma-yielding
let a be set ; :: according to GROUP_7:def 1 :: thesis: ( a in rng (I --> H) implies a is non empty multMagma )
assume a in rng (I --> H) ; :: thesis: a is non empty multMagma
then A1: ex x being set st
( x in dom (I --> H) & a = (I --> H) . x ) by FUNCT_1:def 5;
thus a is non empty multMagma by A1, FUNCOP_1:13; :: thesis: verum