let G be Group; :: thesis: for q being set
for F being Group-like associative multMagma-Family of {q}
for f being Function of G,(product F) st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is bijective
let q be set ; :: thesis: for F being Group-like associative multMagma-Family of {q}
for f being Function of G,(product F) st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is bijective
let F be Group-like associative multMagma-Family of {q}; :: thesis: for f being Function of G,(product F) st F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) holds
f is bijective
let f be Function of G,(product F); :: thesis: ( F = q .--> G & ( for x being Element of G holds f . x = q .--> x ) implies f is bijective )
assume A1: F = q .--> G ; :: thesis: ( ex x being Element of G st not f . x = q .--> x or f is bijective )
assume A2: for x being Element of G holds f . x = q .--> x ; :: thesis: f is bijective
A3: q in {q} by TARSKI:def 1;
A4: 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, A3;
then A5: (Carrier F) . q = the carrier of G by A1, FUNCOP_1:7, A3;
A6: dom (Carrier F) = {q} by PARTFUN1:def 2;
for x1, x2 being object st x1 in the carrier of G & x2 in the carrier of G & f . x1 = f . x2 holds
x1 = x2

proof

let z1, z2 be object ; :: thesis: ( z1 in the carrier of G & z2 in the carrier of G & f . z1 = f . z2 implies z1 = z2 )
assume A7: ( z1 in the carrier of G & z2 in the carrier of G & f . z1 = f . z2 ) ; :: thesis: z1 = z2
then reconsider x1 = z1, x2 = z2 as Element of G ;
A8: f . x2 = q .--> x2 by A2;
thus z1 = (q .--> x1) . q by FUNCOP_1:7, A3
.= (q .--> x2) . q by A8, A2, A7
.= z2 by FUNCOP_1:7, A3 ; :: thesis: verum

end;

then A9: f is one-to-one by FUNCT_2:19;
for y being object st y in the carrier of (product F) holds
ex x being object st
( x in the carrier of G & y = f . x )

proof

let y be object ; :: thesis: ( y in the carrier of (product F) implies ex x being object st
( x in the carrier of G & y = f . x ) )
assume y in the carrier of (product F) ; :: thesis: ex x being object st
( x in the carrier of G & y = f . x )
then consider g being Function such that
A10: ( y = g & dom g = dom (Carrier F) & ( for z being object st z in dom (Carrier F) holds
g . z in (Carrier F) . z ) ) by CARD_3:def 5, A4;
reconsider x = g . q as Element of G by A5, A10, A3, A6;
A11: for z being object st z in dom g holds
g . z = x by TARSKI:def 1, A10;
take x ; :: thesis: ( x in the carrier of G & y = f . x )
thus x in the carrier of G ; :: thesis: y = f . x
thus y = (dom g) --> x by A11, FUNCOP_1:11, A10
.= q .--> x by A10, PARTFUN1:def 2
.= f . x by A2 ; :: thesis: verum

end;

then rng f = the carrier of (product F) by FUNCT_2:10;
then f is onto by FUNCT_2:def 3;
hence f is bijective by A9; :: thesis: verum