let q be set ; :: thesis: for F being Group-like associative multMagma-Family of {q}
for G being Group st F = q .--> G holds
ex HFG being Homomorphism of (),G st
( HFG is bijective & ( for x being {q} -defined the carrier of b2 -valued total Function holds HFG . x = Product x ) )

let F be Group-like associative multMagma-Family of {q}; :: thesis: for G being Group st F = q .--> G holds
ex HFG being Homomorphism of (),G st
( HFG is bijective & ( for x being {q} -defined the carrier of b1 -valued total Function holds HFG . x = Product x ) )

let G be Group; :: thesis: ( F = q .--> G implies ex HFG being Homomorphism of (),G st
( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) ) )

assume A1: F = q .--> G ; :: thesis: ex HFG being Homomorphism of (),G st
( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) )

consider I being Homomorphism of G,() such that
A2: ( I is bijective & ( for x being Element of G holds I . x = q .--> x ) ) by ;
set HFG = I " ;
A3: rng I = the carrier of () by ;
then reconsider HFG = I " as Function of (),G by ;
A4: ( HFG * I = id the carrier of G & I * HFG = id the carrier of () ) by ;
A5: HFG is onto by ;
reconsider HFG = HFG as Homomorphism of (),G by ;
for y being {q} -defined the carrier of G -valued total Function holds HFG . y = Product y
proof
let y be {q} -defined the carrier of G -valued total Function; :: thesis: HFG . y = Product y
A6: ( y in the carrier of () & y . q in the carrier of G & y = q .--> (y . q) ) by ;
reconsider z = y . q as Element of G by ;
A7: I . z = q .--> z by A2
.= y by ;
thus HFG . y = z by
.= Product y by ; :: thesis: verum
end;
hence ex HFG being Homomorphism of (),G st
( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) ) by A5, A2; :: thesis: verum