let A be Group; :: thesis: A, multMagma(# the carrier of A, the multF of A #) are_isomorphic
set G = multMagma(# the carrier of A, the multF of A #);
ex f being Homomorphism of A,multMagma(# the carrier of A, the multF of A #) st f is bijective

proof

reconsider f = id A as Function of A,multMagma(# the carrier of A, the multF of A #) ;
for a1, a2 being Element of A holds f . (a1 * a2) = (f . a1) * (f . a2) ;
then reconsider f = id A as Homomorphism of A,multMagma(# the carrier of A, the multF of A #) by GROUP_6:def 6;
take f ; :: thesis: f is bijective
thus f is bijective ; :: thesis: verum

end;

hence A, multMagma(# the carrier of A, the multF of A #) are_isomorphic by GROUP_6:def 11; :: thesis: verum