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

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

let i be set ; :: thesis: ( i in X implies ex M being non empty commutative multMagma st M = F . i )
assume A2: i in X ; :: thesis: ex M being non empty commutative 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 commutative ; :: thesis: verum