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 I being Homomorphism of G,() st
( I is bijective & ( for x being Element of G holds I . x = q .--> x ) )

let F be Group-like associative multMagma-Family of {q}; :: thesis: for G being Group st F = q .--> G holds
ex I being Homomorphism of G,() st
( I is bijective & ( for x being Element of G holds I . x = q .--> x ) )

let G be Group; :: thesis: ( F = q .--> G implies ex I being Homomorphism of G,() st
( I is bijective & ( for x being Element of G holds I . x = q .--> x ) ) )

assume A1: F = q .--> G ; :: thesis: ex I being Homomorphism of G,() st
( I is bijective & ( for x being Element of G holds I . x = q .--> x ) )

A2: q in {q} by TARSKI:def 1;
A3: the carrier of () = product () by GROUP_7:def 2;
ex R being 1-sorted st
( R = F . q & () . q = the carrier of R ) by ;
then A4: (Carrier F) . q = the carrier of G by ;
A5: dom () = {q} by PARTFUN1:def 2;
defpred S1[ set , set ] means \$2 = q .--> \$1;
A6: for z being Element of G ex w being Element of () st S1[z,w]
proof
let z be Element of G; :: thesis: ex w being Element of () st S1[z,w]
set w = q .--> z;
now :: thesis: for i being object st i in dom (q .--> z) holds
(q .--> z) . i in () . i
let i be object ; :: thesis: ( i in dom (q .--> z) implies (q .--> z) . i in () . i )
assume A8: i in dom (q .--> z) ; :: thesis: (q .--> z) . i in () . i
then A9: i = q by TARSKI:def 1;
(q .--> z) . i = z by ;
hence (q .--> z) . i in () . i by A4, A9; :: thesis: verum
end;
then q .--> z in product () by ;
hence ex w being Element of () st S1[z,w] by A3; :: thesis: verum
end;
consider I being Function of G,() such that
A10: for x being Element of G holds S1[x,I . x] from reconsider I = I as Homomorphism of G,() by ;
I is bijective by ;
hence ex I being Homomorphism of G,() st
( I is bijective & ( for x being Element of G holds I . x = q .--> x ) ) by A10; :: thesis: verum