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

proof

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

end;

then reconsider f = I --> H as multMagma-Family of ;
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 A2: 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 A2;
reconsider F1 = f as multMagma-Family of ;
reconsider Fi = F1 . i1 as non empty Group-like multMagma by FUNCOP_1:13;
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 A3: 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 A3;
reconsider F1 = f as multMagma-Family of ;
reconsider Fi = F1 . i1 as non empty associative multMagma by FUNCOP_1:13;
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 A4: 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 A4;
reconsider F1 = f as multMagma-Family of ;
reconsider Fi = F1 . i1 as non empty commutative multMagma by FUNCOP_1:13;
take Fi ; :: thesis: Fi = f . i
thus Fi = f . i ; :: thesis: verum