set H = the commutative Group;

set f = I --> the commutative Group;

I --> the commutative Group is multMagma-yielding

take f ; :: thesis: ( f is Group-like & f is associative & f is commutative )

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

set f = I --> the commutative Group;

I --> the commutative Group is multMagma-yielding

proof

then reconsider f = I --> the commutative Group as multMagma-Family of I ;
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;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

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;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

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

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 )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;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

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