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,(product F) 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,(product F) 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,(product F) 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,(product F) 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 F) = product (Carrier F) by GROUP_7:def 2;
ex R being 1-sorted st
( R = F . q & (Carrier F) . q = the carrier of R ) by PRALG_1:def 15, A2;
then A4: (Carrier F) . q = the carrier of G by A1, FUNCOP_1:7, A2;
A5: dom (Carrier F) = {q} by PARTFUN1:def 2;
defpred S₁[ set , set ] means $2 = q .--> $1;
A6: for z being Element of G ex w being Element of (product F) st S₁[z,w]

proof

let z be Element of G; :: thesis: ex w being Element of (product F) st S₁[z,w]
set w = q .--> z;

now :: thesis: for i being object st i in dom (q .--> z) holds
(q .--> z) . i in (Carrier F) . i

let i be object ; :: thesis: ( i in dom (q .--> z) implies (q .--> z) . i in (Carrier F) . i )
assume A8: i in dom (q .--> z) ; :: thesis: (q .--> z) . i in (Carrier F) . i
then A9: i = q by TARSKI:def 1;
(q .--> z) . i = z by FUNCOP_1:7, A8;
hence (q .--> z) . i in (Carrier F) . i by A4, A9; :: thesis: verum

end;

then q .--> z in product (Carrier F) by A5, CARD_3:9;
hence ex w being Element of (product F) st S₁[z,w] by A3; :: thesis: verum

end;

consider I being Function of G,(product F) such that
A10: for x being Element of G holds S₁[x,I . x] from FUNCT_2:sch 3(A6);
reconsider I = I as Homomorphism of G,(product F) by Th19, A1, A10;
I is bijective by Th20, A1, A10;
hence ex I being Homomorphism of G,(product F) st
( I is bijective & ( for x being Element of G holds I . x = q .--> x ) ) by A10; :: thesis: verum