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_{1}[ set , set ] means $2 = q .--> $1;

A6: for z being Element of G ex w being Element of (product F) st S_{1}[z,w]

A10: for x being Element of G holds S_{1}[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

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

A6: for z being Element of G ex w being Element of (product F) st S

proof

consider I being Function of G,(product F) such that
let z be Element of G; :: thesis: ex w being Element of (product F) st S_{1}[z,w]

set w = q .--> z;

hence ex w being Element of (product F) st S_{1}[z,w]
by A3; :: thesis: verum

end;set w = q .--> z;

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

(q .--> z) . i in (Carrier F) . i

then
q .--> z in product (Carrier F)
by A5, CARD_3:9;(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;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

hence ex w being Element of (product F) st S

A10: for x being Element of G holds S

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