set H = the non empty multMagma ;
set f = I --> the non empty multMagma ;
take I --> the non empty multMagma ; :: thesis: I --> the non empty multMagma is multMagma-yielding
let a be set ; :: according to GROUP_7:def 1 :: thesis: ( a in rng (I --> the non empty multMagma ) implies a is non empty multMagma )
assume a in rng (I --> the non empty multMagma ) ; :: thesis: a is non empty multMagma
then ex x being object st
( x in dom (I --> the non empty multMagma ) & a = (I --> the non empty multMagma ) . x ) by FUNCT_1:def 3;
hence a is non empty multMagma by FUNCOP_1:7; :: thesis: verum