set H = the commutative Group;
set f = I --> the commutative Group;
I --> the commutative Group is multMagma-yielding

proof

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

end;

then reconsider f = I --> the commutative Group as multMagma-Family of I ;
take f ; :: thesis: ( f is Group-like & f is associative & f is commutative )

hereby :: according to GROUP_7:def 3 :: thesis: ( f is associative & f is commutative )

let i be set ; :: thesis: ( i in I implies ex Fi being non empty Group-like multMagma st Fi = f . i )
assume A1: i in I ; :: thesis: ex Fi being non empty Group-like multMagma st Fi = f . i
then reconsider I1 = I as non empty set ;
reconsider i1 = i as Element of I1 by A1;
reconsider F1 = f as multMagma-Family of I1 ;
reconsider Fi = F1 . i1 as non empty Group-like multMagma ;
take Fi = Fi; :: thesis: Fi = f . i
thus Fi = f . i ; :: thesis: verum

end;

hereby :: according to GROUP_7:def 4 :: thesis: f is commutative

let i be set ; :: thesis: ( i in I implies ex Fi being non empty associative multMagma st Fi = f . i )
assume A2: i in I ; :: thesis: ex Fi being non empty associative multMagma st Fi = f . i
then reconsider I1 = I as non empty set ;
reconsider i1 = i as Element of I1 by A2;
reconsider F1 = f as multMagma-Family of I1 ;
reconsider Fi = F1 . i1 as non empty associative multMagma ;
take Fi = Fi; :: thesis: Fi = f . i
thus Fi = f . i ; :: thesis: verum

end;

let i be set ; :: according to GROUP_7:def 5 :: thesis: ( i in I implies ex Fi being non empty commutative multMagma st Fi = f . i )
assume A3: i in I ; :: thesis: ex Fi being non empty commutative multMagma st Fi = f . i
then reconsider I1 = I as non empty set ;
reconsider i1 = i as Element of I1 by A3;
reconsider F1 = f as multMagma-Family of I1 ;
reconsider Fi = F1 . i1 as non empty commutative multMagma ;
take Fi ; :: thesis: Fi = f . i
thus Fi = f . i ; :: thesis: verum