thus for F being multMagma-Family of I st F is Group-yielding holds
( F is Group-like & F is associative ) :: thesis: verum

proof

let F be multMagma-Family of I; :: thesis: ( F is Group-yielding implies ( F is Group-like & F is associative ) )
assume A1: F is Group-yielding ; :: thesis: ( F is Group-like & F is associative )
A2: dom F = I by PARTFUN1:def 2;
A3: for i being set st i in I holds
ex Fi being non empty Group-like multMagma st Fi = F . i

proof

let i be set ; :: thesis: ( i in I implies ex Fi being non empty Group-like multMagma st Fi = F . i )
assume i in I ; :: thesis: ex Fi being non empty Group-like multMagma st Fi = F . i
then F . i is Group by A1, A2, FUNCT_1:3;
hence ex Fi being non empty Group-like multMagma st Fi = F . i ; :: thesis: verum

end;

for i being set st i in I holds
ex Fi being non empty associative multMagma st Fi = F . i

proof

let i be set ; :: thesis: ( i in I implies ex Fi being non empty associative multMagma st Fi = F . i )
assume i in I ; :: thesis: ex Fi being non empty associative multMagma st Fi = F . i
then F . i is Group by A1, A2, FUNCT_1:3;
hence ex Fi being non empty associative multMagma st Fi = F . i ; :: thesis: verum

end;

hence ( F is Group-like & F is associative ) by A3, GROUP_7:def 3, GROUP_7:def 4; :: thesis: verum

end;