let F be multMagma-Family of X; :: thesis: ( F = X --> M implies F is Group-like )
assume A1: F = X --> M ; :: thesis: F is Group-like

now :: thesis: for i being set st i in X holds
ex M being non empty Group-like multMagma st M = F . i

let i be set ; :: thesis: ( i in X implies ex M being non empty Group-like multMagma st M = F . i )
assume A2: i in X ; :: thesis: ex M being non empty Group-like multMagma st M = F . i
take M = M; :: thesis: M = F . i
thus M = F . i by A1, A2, FUNCOP_1:7; :: thesis: verum

end;

hence F is Group-like ; :: thesis: verum